%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG038+1 : TPTP v9.3.1. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Sun Sep 27 06:47:07 AM UTC 2026 % Result : Theorem 43.73s 6.94s % Output : CNFRefutation 43.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : ALG038+1 : TPTP v9.3.1. Released v2.7.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.11/0.36 % Computer : n007.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Sat Sep 26 20:59:24 UTC 2026 % 0.11/0.36 % CPUTime : % 0.11/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 43.73/6.94 % SZS status Theorem for theBenchmark.p % 43.73/6.94 % SZS output start CNFRefutation for theBenchmark.p % 43.73/6.94 fof(ax1, axiom, ((op1(e10,e10) = e10 | (op1(e10,e10) = e11 | (op1(e10,e10) = e12 | op1(e10,e10) = e13))) & ((op1(e10,e11) = e10 | (op1(e10,e11) = e11 | (op1(e10,e11) = e12 | op1(e10,e11) = e13))) & ((op1(e10,e12) = e10 | (op1(e10,e12) = e11 | (op1(e10,e12) = e12 | op1(e10,e12) = e13))) & ((op1(e10,e13) = e10 | (op1(e10,e13) = e11 | (op1(e10,e13) = e12 | op1(e10,e13) = e13))) & ((op1(e11,e10) = e10 | (op1(e11,e10) = e11 | (op1(e11,e10) = e12 | op1(e11,e10) = e13))) & ((op1(e11,e11) = e10 | (op1(e11,e11) = e11 | (op1(e11,e11) = e12 | op1(e11,e11) = e13))) & ((op1(e11,e12) = e10 | (op1(e11,e12) = e11 | (op1(e11,e12) = e12 | op1(e11,e12) = e13))) & ((op1(e11,e13) = e10 | (op1(e11,e13) = e11 | (op1(e11,e13) = e12 | op1(e11,e13) = e13))) & ((op1(e12,e10) = e10 | (op1(e12,e10) = e11 | (op1(e12,e10) = e12 | op1(e12,e10) = e13))) & ((op1(e12,e11) = e10 | (op1(e12,e11) = e11 | (op1(e12,e11) = e12 | op1(e12,e11) = e13))) & ((op1(e12,e12) = e10 | (op1(e12,e12) = e11 | (op1(e12,e12) = e12 | op1(e12,e12) = e13))) & ((op1(e12,e13) = e10 | (op1(e12,e13) = e11 | (op1(e12,e13) = e12 | op1(e12,e13) = e13))) & ((op1(e13,e10) = e10 | (op1(e13,e10) = e11 | (op1(e13,e10) = e12 | op1(e13,e10) = e13))) & ((op1(e13,e11) = e10 | (op1(e13,e11) = e11 | (op1(e13,e11) = e12 | op1(e13,e11) = e13))) & ((op1(e13,e12) = e10 | (op1(e13,e12) = e11 | (op1(e13,e12) = e12 | op1(e13,e12) = e13))) & (op1(e13,e13) = e10 | (op1(e13,e13) = e11 | (op1(e13,e13) = e12 | op1(e13,e13) = e13))))))))))))))))))). % 43.73/6.94 fof(ax2, axiom, (op1(unit1,e10) = e10 & (op1(e10,unit1) = e10 & (op1(unit1,e11) = e11 & (op1(e11,unit1) = e11 & (op1(unit1,e12) = e12 & (op1(e12,unit1) = e12 & (op1(unit1,e13) = e13 & (op1(e13,unit1) = e13 & (unit1 = e10 | (unit1 = e11 | (unit1 = e12 | unit1 = e13)))))))))))). % 43.73/6.94 fof(ax3, axiom, ((op1(e10,e10) = e10 | (op1(e10,e11) = e10 | (op1(e10,e12) = e10 | op1(e10,e13) = e10))) & ((op1(e10,e10) = e10 | (op1(e11,e10) = e10 | (op1(e12,e10) = e10 | op1(e13,e10) = e10))) & ((op1(e10,e10) = e11 | (op1(e10,e11) = e11 | (op1(e10,e12) = e11 | op1(e10,e13) = e11))) & ((op1(e10,e10) = e11 | (op1(e11,e10) = e11 | (op1(e12,e10) = e11 | op1(e13,e10) = e11))) & ((op1(e10,e10) = e12 | (op1(e10,e11) = e12 | (op1(e10,e12) = e12 | op1(e10,e13) = e12))) & ((op1(e10,e10) = e12 | (op1(e11,e10) = e12 | (op1(e12,e10) = e12 | op1(e13,e10) = e12))) & ((op1(e10,e10) = e13 | (op1(e10,e11) = e13 | (op1(e10,e12) = e13 | op1(e10,e13) = e13))) & ((op1(e10,e10) = e13 | (op1(e11,e10) = e13 | (op1(e12,e10) = e13 | op1(e13,e10) = e13))) & ((op1(e11,e10) = e10 | (op1(e11,e11) = e10 | (op1(e11,e12) = e10 | op1(e11,e13) = e10))) & ((op1(e10,e11) = e10 | (op1(e11,e11) = e10 | (op1(e12,e11) = e10 | op1(e13,e11) = e10))) & ((op1(e11,e10) = e11 | (op1(e11,e11) = e11 | (op1(e11,e12) = e11 | op1(e11,e13) = e11))) & ((op1(e10,e11) = e11 | (op1(e11,e11) = e11 | (op1(e12,e11) = e11 | op1(e13,e11) = e11))) & ((op1(e11,e10) = e12 | (op1(e11,e11) = e12 | (op1(e11,e12) = e12 | op1(e11,e13) = e12))) & ((op1(e10,e11) = e12 | (op1(e11,e11) = e12 | (op1(e12,e11) = e12 | op1(e13,e11) = e12))) & ((op1(e11,e10) = e13 | (op1(e11,e11) = e13 | (op1(e11,e12) = e13 | op1(e11,e13) = e13))) & ((op1(e10,e11) = e13 | (op1(e11,e11) = e13 | (op1(e12,e11) = e13 | op1(e13,e11) = e13))) & ((op1(e12,e10) = e10 | (op1(e12,e11) = e10 | (op1(e12,e12) = e10 | op1(e12,e13) = e10))) & ((op1(e10,e12) = e10 | (op1(e11,e12) = e10 | (op1(e12,e12) = e10 | op1(e13,e12) = e10))) & ((op1(e12,e10) = e11 | (op1(e12,e11) = e11 | (op1(e12,e12) = e11 | op1(e12,e13) = e11))) & ((op1(e10,e12) = e11 | (op1(e11,e12) = e11 | (op1(e12,e12) = e11 | op1(e13,e12) = e11))) & ((op1(e12,e10) = e12 | (op1(e12,e11) = e12 | (op1(e12,e12) = e12 | op1(e12,e13) = e12))) & ((op1(e10,e12) = e12 | (op1(e11,e12) = e12 | (op1(e12,e12) = e12 | op1(e13,e12) = e12))) & ((op1(e12,e10) = e13 | (op1(e12,e11) = e13 | (op1(e12,e12) = e13 | op1(e12,e13) = e13))) & ((op1(e10,e12) = e13 | (op1(e11,e12) = e13 | (op1(e12,e12) = e13 | op1(e13,e12) = e13))) & ((op1(e13,e10) = e10 | (op1(e13,e11) = e10 | (op1(e13,e12) = e10 | op1(e13,e13) = e10))) & ((op1(e10,e13) = e10 | (op1(e11,e13) = e10 | (op1(e12,e13) = e10 | op1(e13,e13) = e10))) & ((op1(e13,e10) = e11 | (op1(e13,e11) = e11 | (op1(e13,e12) = e11 | op1(e13,e13) = e11))) & ((op1(e10,e13) = e11 | (op1(e11,e13) = e11 | (op1(e12,e13) = e11 | op1(e13,e13) = e11))) & ((op1(e13,e10) = e12 | (op1(e13,e11) = e12 | (op1(e13,e12) = e12 | op1(e13,e13) = e12))) & ((op1(e10,e13) = e12 | (op1(e11,e13) = e12 | (op1(e12,e13) = e12 | op1(e13,e13) = e12))) & ((op1(e13,e10) = e13 | (op1(e13,e11) = e13 | (op1(e13,e12) = e13 | op1(e13,e13) = e13))) & (op1(e10,e13) = e13 | (op1(e11,e13) = e13 | (op1(e12,e13) = e13 | op1(e13,e13) = e13))))))))))))))))))))))))))))))))))). % 43.73/6.94 fof(ax4, axiom, ((op2(e20,e20) = e20 | (op2(e20,e20) = e21 | (op2(e20,e20) = e22 | op2(e20,e20) = e23))) & ((op2(e20,e21) = e20 | (op2(e20,e21) = e21 | (op2(e20,e21) = e22 | op2(e20,e21) = e23))) & ((op2(e20,e22) = e20 | (op2(e20,e22) = e21 | (op2(e20,e22) = e22 | op2(e20,e22) = e23))) & ((op2(e20,e23) = e20 | (op2(e20,e23) = e21 | (op2(e20,e23) = e22 | op2(e20,e23) = e23))) & ((op2(e21,e20) = e20 | (op2(e21,e20) = e21 | (op2(e21,e20) = e22 | op2(e21,e20) = e23))) & ((op2(e21,e21) = e20 | (op2(e21,e21) = e21 | (op2(e21,e21) = e22 | op2(e21,e21) = e23))) & ((op2(e21,e22) = e20 | (op2(e21,e22) = e21 | (op2(e21,e22) = e22 | op2(e21,e22) = e23))) & ((op2(e21,e23) = e20 | (op2(e21,e23) = e21 | (op2(e21,e23) = e22 | op2(e21,e23) = e23))) & ((op2(e22,e20) = e20 | (op2(e22,e20) = e21 | (op2(e22,e20) = e22 | op2(e22,e20) = e23))) & ((op2(e22,e21) = e20 | (op2(e22,e21) = e21 | (op2(e22,e21) = e22 | op2(e22,e21) = e23))) & ((op2(e22,e22) = e20 | (op2(e22,e22) = e21 | (op2(e22,e22) = e22 | op2(e22,e22) = e23))) & ((op2(e22,e23) = e20 | (op2(e22,e23) = e21 | (op2(e22,e23) = e22 | op2(e22,e23) = e23))) & ((op2(e23,e20) = e20 | (op2(e23,e20) = e21 | (op2(e23,e20) = e22 | op2(e23,e20) = e23))) & ((op2(e23,e21) = e20 | (op2(e23,e21) = e21 | (op2(e23,e21) = e22 | op2(e23,e21) = e23))) & ((op2(e23,e22) = e20 | (op2(e23,e22) = e21 | (op2(e23,e22) = e22 | op2(e23,e22) = e23))) & (op2(e23,e23) = e20 | (op2(e23,e23) = e21 | (op2(e23,e23) = e22 | op2(e23,e23) = e23))))))))))))))))))). % 43.73/6.94 fof(ax5, axiom, (op2(unit2,e20) = e20 & (op2(e20,unit2) = e20 & (op2(unit2,e21) = e21 & (op2(e21,unit2) = e21 & (op2(unit2,e22) = e22 & (op2(e22,unit2) = e22 & (op2(unit2,e23) = e23 & (op2(e23,unit2) = e23 & (unit2 = e20 | (unit2 = e21 | (unit2 = e22 | unit2 = e23)))))))))))). % 43.73/6.94 fof(ax6, axiom, ((op2(e20,e20) = e20 | (op2(e20,e21) = e20 | (op2(e20,e22) = e20 | op2(e20,e23) = e20))) & ((op2(e20,e20) = e20 | (op2(e21,e20) = e20 | (op2(e22,e20) = e20 | op2(e23,e20) = e20))) & ((op2(e20,e20) = e21 | (op2(e20,e21) = e21 | (op2(e20,e22) = e21 | op2(e20,e23) = e21))) & ((op2(e20,e20) = e21 | (op2(e21,e20) = e21 | (op2(e22,e20) = e21 | op2(e23,e20) = e21))) & ((op2(e20,e20) = e22 | (op2(e20,e21) = e22 | (op2(e20,e22) = e22 | op2(e20,e23) = e22))) & ((op2(e20,e20) = e22 | (op2(e21,e20) = e22 | (op2(e22,e20) = e22 | op2(e23,e20) = e22))) & ((op2(e20,e20) = e23 | (op2(e20,e21) = e23 | (op2(e20,e22) = e23 | op2(e20,e23) = e23))) & ((op2(e20,e20) = e23 | (op2(e21,e20) = e23 | (op2(e22,e20) = e23 | op2(e23,e20) = e23))) & ((op2(e21,e20) = e20 | (op2(e21,e21) = e20 | (op2(e21,e22) = e20 | op2(e21,e23) = e20))) & ((op2(e20,e21) = e20 | (op2(e21,e21) = e20 | (op2(e22,e21) = e20 | op2(e23,e21) = e20))) & ((op2(e21,e20) = e21 | (op2(e21,e21) = e21 | (op2(e21,e22) = e21 | op2(e21,e23) = e21))) & ((op2(e20,e21) = e21 | (op2(e21,e21) = e21 | (op2(e22,e21) = e21 | op2(e23,e21) = e21))) & ((op2(e21,e20) = e22 | (op2(e21,e21) = e22 | (op2(e21,e22) = e22 | op2(e21,e23) = e22))) & ((op2(e20,e21) = e22 | (op2(e21,e21) = e22 | (op2(e22,e21) = e22 | op2(e23,e21) = e22))) & ((op2(e21,e20) = e23 | (op2(e21,e21) = e23 | (op2(e21,e22) = e23 | op2(e21,e23) = e23))) & ((op2(e20,e21) = e23 | (op2(e21,e21) = e23 | (op2(e22,e21) = e23 | op2(e23,e21) = e23))) & ((op2(e22,e20) = e20 | (op2(e22,e21) = e20 | (op2(e22,e22) = e20 | op2(e22,e23) = e20))) & ((op2(e20,e22) = e20 | (op2(e21,e22) = e20 | (op2(e22,e22) = e20 | op2(e23,e22) = e20))) & ((op2(e22,e20) = e21 | (op2(e22,e21) = e21 | (op2(e22,e22) = e21 | op2(e22,e23) = e21))) & ((op2(e20,e22) = e21 | (op2(e21,e22) = e21 | (op2(e22,e22) = e21 | op2(e23,e22) = e21))) & ((op2(e22,e20) = e22 | (op2(e22,e21) = e22 | (op2(e22,e22) = e22 | op2(e22,e23) = e22))) & ((op2(e20,e22) = e22 | (op2(e21,e22) = e22 | (op2(e22,e22) = e22 | op2(e23,e22) = e22))) & ((op2(e22,e20) = e23 | (op2(e22,e21) = e23 | (op2(e22,e22) = e23 | op2(e22,e23) = e23))) & ((op2(e20,e22) = e23 | (op2(e21,e22) = e23 | (op2(e22,e22) = e23 | op2(e23,e22) = e23))) & ((op2(e23,e20) = e20 | (op2(e23,e21) = e20 | (op2(e23,e22) = e20 | op2(e23,e23) = e20))) & ((op2(e20,e23) = e20 | (op2(e21,e23) = e20 | (op2(e22,e23) = e20 | op2(e23,e23) = e20))) & ((op2(e23,e20) = e21 | (op2(e23,e21) = e21 | (op2(e23,e22) = e21 | op2(e23,e23) = e21))) & ((op2(e20,e23) = e21 | (op2(e21,e23) = e21 | (op2(e22,e23) = e21 | op2(e23,e23) = e21))) & ((op2(e23,e20) = e22 | (op2(e23,e21) = e22 | (op2(e23,e22) = e22 | op2(e23,e23) = e22))) & ((op2(e20,e23) = e22 | (op2(e21,e23) = e22 | (op2(e22,e23) = e22 | op2(e23,e23) = e22))) & ((op2(e23,e20) = e23 | (op2(e23,e21) = e23 | (op2(e23,e22) = e23 | op2(e23,e23) = e23))) & (op2(e20,e23) = e23 | (op2(e21,e23) = e23 | (op2(e22,e23) = e23 | op2(e23,e23) = e23))))))))))))))))))))))))))))))))))). % 43.73/6.94 fof(ax7, axiom, (op1(e10,e10) != op1(e11,e10) & (op1(e10,e10) != op1(e12,e10) & (op1(e10,e10) != op1(e13,e10) & (op1(e11,e10) != op1(e12,e10) & (op1(e11,e10) != op1(e13,e10) & (op1(e12,e10) != op1(e13,e10) & (op1(e10,e11) != op1(e11,e11) & (op1(e10,e11) != op1(e12,e11) & (op1(e10,e11) != op1(e13,e11) & (op1(e11,e11) != op1(e12,e11) & (op1(e11,e11) != op1(e13,e11) & (op1(e12,e11) != op1(e13,e11) & (op1(e10,e12) != op1(e11,e12) & (op1(e10,e12) != op1(e12,e12) & (op1(e10,e12) != op1(e13,e12) & (op1(e11,e12) != op1(e12,e12) & (op1(e11,e12) != op1(e13,e12) & (op1(e12,e12) != op1(e13,e12) & (op1(e10,e13) != op1(e11,e13) & (op1(e10,e13) != op1(e12,e13) & (op1(e10,e13) != op1(e13,e13) & (op1(e11,e13) != op1(e12,e13) & (op1(e11,e13) != op1(e13,e13) & (op1(e12,e13) != op1(e13,e13) & (op1(e10,e10) != op1(e10,e11) & (op1(e10,e10) != op1(e10,e12) & (op1(e10,e10) != op1(e10,e13) & (op1(e10,e11) != op1(e10,e12) & (op1(e10,e11) != op1(e10,e13) & (op1(e10,e12) != op1(e10,e13) & (op1(e11,e10) != op1(e11,e11) & (op1(e11,e10) != op1(e11,e12) & (op1(e11,e10) != op1(e11,e13) & (op1(e11,e11) != op1(e11,e12) & (op1(e11,e11) != op1(e11,e13) & (op1(e11,e12) != op1(e11,e13) & (op1(e12,e10) != op1(e12,e11) & (op1(e12,e10) != op1(e12,e12) & (op1(e12,e10) != op1(e12,e13) & (op1(e12,e11) != op1(e12,e12) & (op1(e12,e11) != op1(e12,e13) & (op1(e12,e12) != op1(e12,e13) & (op1(e13,e10) != op1(e13,e11) & (op1(e13,e10) != op1(e13,e12) & (op1(e13,e10) != op1(e13,e13) & (op1(e13,e11) != op1(e13,e12) & (op1(e13,e11) != op1(e13,e13) & op1(e13,e12) != op1(e13,e13))))))))))))))))))))))))))))))))))))))))))))))))). % 43.73/6.94 fof(ax8, axiom, (op2(e20,e20) != op2(e21,e20) & (op2(e20,e20) != op2(e22,e20) & (op2(e20,e20) != op2(e23,e20) & (op2(e21,e20) != op2(e22,e20) & (op2(e21,e20) != op2(e23,e20) & (op2(e22,e20) != op2(e23,e20) & (op2(e20,e21) != op2(e21,e21) & (op2(e20,e21) != op2(e22,e21) & (op2(e20,e21) != op2(e23,e21) & (op2(e21,e21) != op2(e22,e21) & (op2(e21,e21) != op2(e23,e21) & (op2(e22,e21) != op2(e23,e21) & (op2(e20,e22) != op2(e21,e22) & (op2(e20,e22) != op2(e22,e22) & (op2(e20,e22) != op2(e23,e22) & (op2(e21,e22) != op2(e22,e22) & (op2(e21,e22) != op2(e23,e22) & (op2(e22,e22) != op2(e23,e22) & (op2(e20,e23) != op2(e21,e23) & (op2(e20,e23) != op2(e22,e23) & (op2(e20,e23) != op2(e23,e23) & (op2(e21,e23) != op2(e22,e23) & (op2(e21,e23) != op2(e23,e23) & (op2(e22,e23) != op2(e23,e23) & (op2(e20,e20) != op2(e20,e21) & (op2(e20,e20) != op2(e20,e22) & (op2(e20,e20) != op2(e20,e23) & (op2(e20,e21) != op2(e20,e22) & (op2(e20,e21) != op2(e20,e23) & (op2(e20,e22) != op2(e20,e23) & (op2(e21,e20) != op2(e21,e21) & (op2(e21,e20) != op2(e21,e22) & (op2(e21,e20) != op2(e21,e23) & (op2(e21,e21) != op2(e21,e22) & (op2(e21,e21) != op2(e21,e23) & (op2(e21,e22) != op2(e21,e23) & (op2(e22,e20) != op2(e22,e21) & (op2(e22,e20) != op2(e22,e22) & (op2(e22,e20) != op2(e22,e23) & (op2(e22,e21) != op2(e22,e22) & (op2(e22,e21) != op2(e22,e23) & (op2(e22,e22) != op2(e22,e23) & (op2(e23,e20) != op2(e23,e21) & (op2(e23,e20) != op2(e23,e22) & (op2(e23,e20) != op2(e23,e23) & (op2(e23,e21) != op2(e23,e22) & (op2(e23,e21) != op2(e23,e23) & op2(e23,e22) != op2(e23,e23))))))))))))))))))))))))))))))))))))))))))))))))). % 43.73/6.94 fof(ax9, axiom, (e10 != e11 & (e10 != e12 & (e10 != e13 & (e11 != e12 & (e11 != e13 & e12 != e13)))))). % 43.73/6.94 fof(ax10, axiom, (e20 != e21 & (e20 != e22 & (e20 != e23 & (e21 != e22 & (e21 != e23 & e22 != e23)))))). % 43.73/6.94 fof(ax14, axiom, (e10 = op1(e11,op1(e11,op1(e11,e11))) & (e12 = op1(e11,op1(e11,e11)) & e13 = op1(e11,e11)))). % 43.73/6.94 fof(ax15, axiom, (e20 = op2(e21,op2(e21,op2(e21,e21))) & (e22 = op2(e21,op2(e21,e21)) & e23 = op2(e21,e21)))). % 43.73/6.94 fof(ax17, axiom, (h2(e11) = e21 & (h2(e10) = op2(e21,op2(e21,op2(e21,e21))) & (h2(e12) = op2(e21,op2(e21,e21)) & h2(e13) = op2(e21,e21))))). % 43.73/6.94 fof(ax18, axiom, (h3(e11) = e22 & (h3(e10) = op2(e22,op2(e22,op2(e22,e22))) & (h3(e12) = op2(e22,op2(e22,e22)) & h3(e13) = op2(e22,e22))))). % 43.73/6.94 fof(ax19, axiom, (h4(e11) = e23 & (h4(e10) = op2(e23,op2(e23,op2(e23,e23))) & (h4(e12) = op2(e23,op2(e23,e23)) & h4(e13) = op2(e23,e23))))). % 43.73/6.94 fof(co1, conjecture, ((h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) & (h1(op1(e10,e11)) = op2(h1(e10),h1(e11)) & (h1(op1(e10,e12)) = op2(h1(e10),h1(e12)) & (h1(op1(e10,e13)) = op2(h1(e10),h1(e13)) & (h1(op1(e11,e10)) = op2(h1(e11),h1(e10)) & (h1(op1(e11,e11)) = op2(h1(e11),h1(e11)) & (h1(op1(e11,e12)) = op2(h1(e11),h1(e12)) & (h1(op1(e11,e13)) = op2(h1(e11),h1(e13)) & (h1(op1(e12,e10)) = op2(h1(e12),h1(e10)) & (h1(op1(e12,e11)) = op2(h1(e12),h1(e11)) & (h1(op1(e12,e12)) = op2(h1(e12),h1(e12)) & (h1(op1(e12,e13)) = op2(h1(e12),h1(e13)) & (h1(op1(e13,e10)) = op2(h1(e13),h1(e10)) & (h1(op1(e13,e11)) = op2(h1(e13),h1(e11)) & (h1(op1(e13,e12)) = op2(h1(e13),h1(e12)) & (h1(op1(e13,e13)) = op2(h1(e13),h1(e13)) & ((h1(e10) = e20 | (h1(e11) = e20 | (h1(e12) = e20 | h1(e13) = e20))) & ((h1(e10) = e21 | (h1(e11) = e21 | (h1(e12) = e21 | h1(e13) = e21))) & ((h1(e10) = e22 | (h1(e11) = e22 | (h1(e12) = e22 | h1(e13) = e22))) & (h1(e10) = e23 | (h1(e11) = e23 | (h1(e12) = e23 | h1(e13) = e23)))))))))))))))))))))) | ((h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) & (h2(op1(e10,e11)) = op2(h2(e10),h2(e11)) & (h2(op1(e10,e12)) = op2(h2(e10),h2(e12)) & (h2(op1(e10,e13)) = op2(h2(e10),h2(e13)) & (h2(op1(e11,e10)) = op2(h2(e11),h2(e10)) & (h2(op1(e11,e11)) = op2(h2(e11),h2(e11)) & (h2(op1(e11,e12)) = op2(h2(e11),h2(e12)) & (h2(op1(e11,e13)) = op2(h2(e11),h2(e13)) & (h2(op1(e12,e10)) = op2(h2(e12),h2(e10)) & (h2(op1(e12,e11)) = op2(h2(e12),h2(e11)) & (h2(op1(e12,e12)) = op2(h2(e12),h2(e12)) & (h2(op1(e12,e13)) = op2(h2(e12),h2(e13)) & (h2(op1(e13,e10)) = op2(h2(e13),h2(e10)) & (h2(op1(e13,e11)) = op2(h2(e13),h2(e11)) & (h2(op1(e13,e12)) = op2(h2(e13),h2(e12)) & (h2(op1(e13,e13)) = op2(h2(e13),h2(e13)) & ((h2(e10) = e20 | (h2(e11) = e20 | (h2(e12) = e20 | h2(e13) = e20))) & ((h2(e10) = e21 | (h2(e11) = e21 | (h2(e12) = e21 | h2(e13) = e21))) & ((h2(e10) = e22 | (h2(e11) = e22 | (h2(e12) = e22 | h2(e13) = e22))) & (h2(e10) = e23 | (h2(e11) = e23 | (h2(e12) = e23 | h2(e13) = e23)))))))))))))))))))))) | ((h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) & (h3(op1(e10,e11)) = op2(h3(e10),h3(e11)) & (h3(op1(e10,e12)) = op2(h3(e10),h3(e12)) & (h3(op1(e10,e13)) = op2(h3(e10),h3(e13)) & (h3(op1(e11,e10)) = op2(h3(e11),h3(e10)) & (h3(op1(e11,e11)) = op2(h3(e11),h3(e11)) & (h3(op1(e11,e12)) = op2(h3(e11),h3(e12)) & (h3(op1(e11,e13)) = op2(h3(e11),h3(e13)) & (h3(op1(e12,e10)) = op2(h3(e12),h3(e10)) & (h3(op1(e12,e11)) = op2(h3(e12),h3(e11)) & (h3(op1(e12,e12)) = op2(h3(e12),h3(e12)) & (h3(op1(e12,e13)) = op2(h3(e12),h3(e13)) & (h3(op1(e13,e10)) = op2(h3(e13),h3(e10)) & (h3(op1(e13,e11)) = op2(h3(e13),h3(e11)) & (h3(op1(e13,e12)) = op2(h3(e13),h3(e12)) & (h3(op1(e13,e13)) = op2(h3(e13),h3(e13)) & ((h3(e10) = e20 | (h3(e11) = e20 | (h3(e12) = e20 | h3(e13) = e20))) & ((h3(e10) = e21 | (h3(e11) = e21 | (h3(e12) = e21 | h3(e13) = e21))) & ((h3(e10) = e22 | (h3(e11) = e22 | (h3(e12) = e22 | h3(e13) = e22))) & (h3(e10) = e23 | (h3(e11) = e23 | (h3(e12) = e23 | h3(e13) = e23)))))))))))))))))))))) | (h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) & (h4(op1(e10,e11)) = op2(h4(e10),h4(e11)) & (h4(op1(e10,e12)) = op2(h4(e10),h4(e12)) & (h4(op1(e10,e13)) = op2(h4(e10),h4(e13)) & (h4(op1(e11,e10)) = op2(h4(e11),h4(e10)) & (h4(op1(e11,e11)) = op2(h4(e11),h4(e11)) & (h4(op1(e11,e12)) = op2(h4(e11),h4(e12)) & (h4(op1(e11,e13)) = op2(h4(e11),h4(e13)) & (h4(op1(e12,e10)) = op2(h4(e12),h4(e10)) & (h4(op1(e12,e11)) = op2(h4(e12),h4(e11)) & (h4(op1(e12,e12)) = op2(h4(e12),h4(e12)) & (h4(op1(e12,e13)) = op2(h4(e12),h4(e13)) & (h4(op1(e13,e10)) = op2(h4(e13),h4(e10)) & (h4(op1(e13,e11)) = op2(h4(e13),h4(e11)) & (h4(op1(e13,e12)) = op2(h4(e13),h4(e12)) & (h4(op1(e13,e13)) = op2(h4(e13),h4(e13)) & ((h4(e10) = e20 | (h4(e11) = e20 | (h4(e12) = e20 | h4(e13) = e20))) & ((h4(e10) = e21 | (h4(e11) = e21 | (h4(e12) = e21 | h4(e13) = e21))) & ((h4(e10) = e22 | (h4(e11) = e22 | (h4(e12) = e22 | h4(e13) = e22))) & (h4(e10) = e23 | (h4(e11) = e23 | (h4(e12) = e23 | h4(e13) = e23)))))))))))))))))))))))))). % 43.73/6.94 fof(negated_conjecture, negated_conjecture, ~(((h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) & (h1(op1(e10,e11)) = op2(h1(e10),h1(e11)) & (h1(op1(e10,e12)) = op2(h1(e10),h1(e12)) & (h1(op1(e10,e13)) = op2(h1(e10),h1(e13)) & (h1(op1(e11,e10)) = op2(h1(e11),h1(e10)) & (h1(op1(e11,e11)) = op2(h1(e11),h1(e11)) & (h1(op1(e11,e12)) = op2(h1(e11),h1(e12)) & (h1(op1(e11,e13)) = op2(h1(e11),h1(e13)) & (h1(op1(e12,e10)) = op2(h1(e12),h1(e10)) & (h1(op1(e12,e11)) = op2(h1(e12),h1(e11)) & (h1(op1(e12,e12)) = op2(h1(e12),h1(e12)) & (h1(op1(e12,e13)) = op2(h1(e12),h1(e13)) & (h1(op1(e13,e10)) = op2(h1(e13),h1(e10)) & (h1(op1(e13,e11)) = op2(h1(e13),h1(e11)) & (h1(op1(e13,e12)) = op2(h1(e13),h1(e12)) & (h1(op1(e13,e13)) = op2(h1(e13),h1(e13)) & ((h1(e10) = e20 | (h1(e11) = e20 | (h1(e12) = e20 | h1(e13) = e20))) & ((h1(e10) = e21 | (h1(e11) = e21 | (h1(e12) = e21 | h1(e13) = e21))) & ((h1(e10) = e22 | (h1(e11) = e22 | (h1(e12) = e22 | h1(e13) = e22))) & (h1(e10) = e23 | (h1(e11) = e23 | (h1(e12) = e23 | h1(e13) = e23)))))))))))))))))))))) | ((h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) & (h2(op1(e10,e11)) = op2(h2(e10),h2(e11)) & (h2(op1(e10,e12)) = op2(h2(e10),h2(e12)) & (h2(op1(e10,e13)) = op2(h2(e10),h2(e13)) & (h2(op1(e11,e10)) = op2(h2(e11),h2(e10)) & (h2(op1(e11,e11)) = op2(h2(e11),h2(e11)) & (h2(op1(e11,e12)) = op2(h2(e11),h2(e12)) & (h2(op1(e11,e13)) = op2(h2(e11),h2(e13)) & (h2(op1(e12,e10)) = op2(h2(e12),h2(e10)) & (h2(op1(e12,e11)) = op2(h2(e12),h2(e11)) & (h2(op1(e12,e12)) = op2(h2(e12),h2(e12)) & (h2(op1(e12,e13)) = op2(h2(e12),h2(e13)) & (h2(op1(e13,e10)) = op2(h2(e13),h2(e10)) & (h2(op1(e13,e11)) = op2(h2(e13),h2(e11)) & (h2(op1(e13,e12)) = op2(h2(e13),h2(e12)) & (h2(op1(e13,e13)) = op2(h2(e13),h2(e13)) & ((h2(e10) = e20 | (h2(e11) = e20 | (h2(e12) = e20 | h2(e13) = e20))) & ((h2(e10) = e21 | (h2(e11) = e21 | (h2(e12) = e21 | h2(e13) = e21))) & ((h2(e10) = e22 | (h2(e11) = e22 | (h2(e12) = e22 | h2(e13) = e22))) & (h2(e10) = e23 | (h2(e11) = e23 | (h2(e12) = e23 | h2(e13) = e23)))))))))))))))))))))) | ((h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) & (h3(op1(e10,e11)) = op2(h3(e10),h3(e11)) & (h3(op1(e10,e12)) = op2(h3(e10),h3(e12)) & (h3(op1(e10,e13)) = op2(h3(e10),h3(e13)) & (h3(op1(e11,e10)) = op2(h3(e11),h3(e10)) & (h3(op1(e11,e11)) = op2(h3(e11),h3(e11)) & (h3(op1(e11,e12)) = op2(h3(e11),h3(e12)) & (h3(op1(e11,e13)) = op2(h3(e11),h3(e13)) & (h3(op1(e12,e10)) = op2(h3(e12),h3(e10)) & (h3(op1(e12,e11)) = op2(h3(e12),h3(e11)) & (h3(op1(e12,e12)) = op2(h3(e12),h3(e12)) & (h3(op1(e12,e13)) = op2(h3(e12),h3(e13)) & (h3(op1(e13,e10)) = op2(h3(e13),h3(e10)) & (h3(op1(e13,e11)) = op2(h3(e13),h3(e11)) & (h3(op1(e13,e12)) = op2(h3(e13),h3(e12)) & (h3(op1(e13,e13)) = op2(h3(e13),h3(e13)) & ((h3(e10) = e20 | (h3(e11) = e20 | (h3(e12) = e20 | h3(e13) = e20))) & ((h3(e10) = e21 | (h3(e11) = e21 | (h3(e12) = e21 | h3(e13) = e21))) & ((h3(e10) = e22 | (h3(e11) = e22 | (h3(e12) = e22 | h3(e13) = e22))) & (h3(e10) = e23 | (h3(e11) = e23 | (h3(e12) = e23 | h3(e13) = e23)))))))))))))))))))))) | (h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) & (h4(op1(e10,e11)) = op2(h4(e10),h4(e11)) & (h4(op1(e10,e12)) = op2(h4(e10),h4(e12)) & (h4(op1(e10,e13)) = op2(h4(e10),h4(e13)) & (h4(op1(e11,e10)) = op2(h4(e11),h4(e10)) & (h4(op1(e11,e11)) = op2(h4(e11),h4(e11)) & (h4(op1(e11,e12)) = op2(h4(e11),h4(e12)) & (h4(op1(e11,e13)) = op2(h4(e11),h4(e13)) & (h4(op1(e12,e10)) = op2(h4(e12),h4(e10)) & (h4(op1(e12,e11)) = op2(h4(e12),h4(e11)) & (h4(op1(e12,e12)) = op2(h4(e12),h4(e12)) & (h4(op1(e12,e13)) = op2(h4(e12),h4(e13)) & (h4(op1(e13,e10)) = op2(h4(e13),h4(e10)) & (h4(op1(e13,e11)) = op2(h4(e13),h4(e11)) & (h4(op1(e13,e12)) = op2(h4(e13),h4(e12)) & (h4(op1(e13,e13)) = op2(h4(e13),h4(e13)) & ((h4(e10) = e20 | (h4(e11) = e20 | (h4(e12) = e20 | h4(e13) = e20))) & ((h4(e10) = e21 | (h4(e11) = e21 | (h4(e12) = e21 | h4(e13) = e21))) & ((h4(e10) = e22 | (h4(e11) = e22 | (h4(e12) = e22 | h4(e13) = e22))) & (h4(e10) = e23 | (h4(e11) = e23 | (h4(e12) = e23 | h4(e13) = e23)))))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 43.73/6.94 cnf(c1, plain, op1(e10,e11) = e10 | op1(e10,e11) = e11 | op1(e10,e11) = e12 | op1(e10,e11) = e13, inference(clausification, [status(esa)], [ax1])). % 43.73/6.94 cnf(c11, plain, op1(e12,e13) = e10 | op1(e12,e13) = e11 | op1(e12,e13) = e12 | op1(e12,e13) = e13, inference(clausification, [status(esa)], [ax1])). % 43.73/6.94 cnf(c15, plain, op1(e13,e13) = e10 | op1(e13,e13) = e11 | op1(e13,e13) = e12 | op1(e13,e13) = e13, inference(clausification, [status(esa)], [ax1])). % 43.73/6.94 cnf(c16, plain, op1(unit1,e10) = e10, inference(clausification, [status(esa)], [ax2])). % 43.73/6.94 cnf(c17, plain, op1(e10,unit1) = e10, inference(clausification, [status(esa)], [ax2])). % 43.73/6.94 cnf(c18, plain, op1(unit1,e11) = e11, inference(clausification, [status(esa)], [ax2])). % 43.73/6.94 cnf(c19, plain, op1(e11,unit1) = e11, inference(clausification, [status(esa)], [ax2])). % 43.73/6.94 cnf(c20, plain, op1(unit1,e12) = e12, inference(clausification, [status(esa)], [ax2])). % 43.73/6.94 cnf(c21, plain, op1(e12,unit1) = e12, inference(clausification, [status(esa)], [ax2])). % 43.73/6.94 cnf(c22, plain, op1(unit1,e13) = e13, inference(clausification, [status(esa)], [ax2])). % 43.73/6.94 cnf(c23, plain, op1(e13,unit1) = e13, inference(clausification, [status(esa)], [ax2])). % 43.73/6.94 cnf(c24, plain, unit1 = e10 | unit1 = e11 | unit1 = e12 | unit1 = e13, inference(clausification, [status(esa)], [ax2])). % 43.73/6.94 cnf(c29, plain, op1(e10,e10) = e12 | op1(e10,e11) = e12 | op1(e10,e12) = e12 | op1(e10,e13) = e12, inference(clausification, [status(esa)], [ax3])). % 43.73/6.94 cnf(c31, plain, op1(e10,e10) = e13 | op1(e10,e11) = e13 | op1(e10,e12) = e13 | op1(e10,e13) = e13, inference(clausification, [status(esa)], [ax3])). % 43.73/6.94 cnf(c34, plain, op1(e10,e11) = e10 | op1(e11,e11) = e10 | op1(e12,e11) = e10 | op1(e13,e11) = e10, inference(clausification, [status(esa)], [ax3])). % 43.73/6.94 cnf(c38, plain, op1(e10,e11) = e12 | op1(e11,e11) = e12 | op1(e12,e11) = e12 | op1(e13,e11) = e12, inference(clausification, [status(esa)], [ax3])). % 43.73/6.94 cnf(c44, plain, op1(e10,e12) = e11 | op1(e11,e12) = e11 | op1(e12,e12) = e11 | op1(e13,e12) = e11, inference(clausification, [status(esa)], [ax3])). % 43.73/6.94 cnf(c47, plain, op1(e12,e10) = e13 | op1(e12,e11) = e13 | op1(e12,e12) = e13 | op1(e12,e13) = e13, inference(clausification, [status(esa)], [ax3])). % 43.73/6.94 cnf(c58, plain, op2(e20,e21) = e20 | op2(e20,e21) = e21 | op2(e20,e21) = e22 | op2(e20,e21) = e23, inference(clausification, [status(esa)], [ax4])). % 43.73/6.94 cnf(c66, plain, op2(e22,e21) = e20 | op2(e22,e21) = e21 | op2(e22,e21) = e22 | op2(e22,e21) = e23, inference(clausification, [status(esa)], [ax4])). % 43.73/6.94 cnf(c74, plain, op2(e20,unit2) = e20, inference(clausification, [status(esa)], [ax5])). % 43.73/6.94 cnf(c75, plain, op2(unit2,e21) = e21, inference(clausification, [status(esa)], [ax5])). % 43.73/6.94 cnf(c76, plain, op2(e21,unit2) = e21, inference(clausification, [status(esa)], [ax5])). % 43.73/6.94 cnf(c77, plain, op2(unit2,e22) = e22, inference(clausification, [status(esa)], [ax5])). % 43.73/6.94 cnf(c78, plain, op2(e22,unit2) = e22, inference(clausification, [status(esa)], [ax5])). % 43.73/6.94 cnf(c79, plain, op2(unit2,e23) = e23, inference(clausification, [status(esa)], [ax5])). % 43.73/6.94 cnf(c80, plain, op2(e23,unit2) = e23, inference(clausification, [status(esa)], [ax5])). % 43.73/6.94 cnf(c81, plain, unit2 = e20 | unit2 = e21 | unit2 = e22 | unit2 = e23, inference(clausification, [status(esa)], [ax5])). % 43.73/6.94 cnf(c86, plain, op2(e20,e20) = e22 | op2(e20,e21) = e22 | op2(e20,e22) = e22 | op2(e20,e23) = e22, inference(clausification, [status(esa)], [ax6])). % 43.73/6.94 cnf(c88, plain, op2(e20,e20) = e23 | op2(e20,e21) = e23 | op2(e20,e22) = e23 | op2(e20,e23) = e23, inference(clausification, [status(esa)], [ax6])). % 43.73/6.94 cnf(c95, plain, op2(e20,e21) = e22 | op2(e21,e21) = e22 | op2(e22,e21) = e22 | op2(e23,e21) = e22, inference(clausification, [status(esa)], [ax6])). % 43.73/6.94 cnf(c100, plain, op2(e22,e20) = e21 | op2(e22,e21) = e21 | op2(e22,e22) = e21 | op2(e22,e23) = e21, inference(clausification, [status(esa)], [ax6])). % 43.73/6.94 cnf(c101, plain, op2(e20,e22) = e21 | op2(e21,e22) = e21 | op2(e22,e22) = e21 | op2(e23,e22) = e21, inference(clausification, [status(esa)], [ax6])). % 43.73/6.94 cnf(c104, plain, op2(e22,e20) = e23 | op2(e22,e21) = e23 | op2(e22,e22) = e23 | op2(e22,e23) = e23, inference(clausification, [status(esa)], [ax6])). % 43.73/6.94 cnf(c106, plain, op2(e23,e20) = e20 | op2(e23,e21) = e20 | op2(e23,e22) = e20 | op2(e23,e23) = e20, inference(clausification, [status(esa)], [ax6])). % 43.73/6.94 cnf(c120, plain, op1(e10,e11) != op1(e11,e11), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c126, plain, op1(e10,e12) != op1(e11,e12), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c133, plain, op1(e10,e13) != op1(e12,e13), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c135, plain, op1(e11,e13) != op1(e12,e13), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c136, plain, op1(e11,e13) != op1(e13,e13), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c137, plain, op1(e12,e13) != op1(e13,e13), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c145, plain, op1(e11,e10) != op1(e11,e12), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c147, plain, op1(e11,e11) != op1(e11,e12), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c148, plain, op1(e11,e11) != op1(e11,e13), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c150, plain, op1(e12,e10) != op1(e12,e11), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c154, plain, op1(e12,e11) != op1(e12,e13), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c155, plain, op1(e12,e12) != op1(e12,e13), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c158, plain, op1(e13,e10) != op1(e13,e13), inference(clausification, [status(esa)], [ax7])). % 43.73/6.94 cnf(c169, plain, op2(e20,e21) != op2(e22,e21), inference(clausification, [status(esa)], [ax8])). % 43.73/6.94 cnf(c171, plain, op2(e21,e21) != op2(e22,e21), inference(clausification, [status(esa)], [ax8])). % 43.73/6.94 cnf(c174, plain, op2(e20,e22) != op2(e21,e22), inference(clausification, [status(esa)], [ax8])). % 43.73/6.94 cnf(c178, plain, op2(e21,e22) != op2(e23,e22), inference(clausification, [status(esa)], [ax8])). % 43.73/6.94 cnf(c181, plain, op2(e20,e23) != op2(e22,e23), inference(clausification, [status(esa)], [ax8])). % 43.73/6.94 cnf(c183, plain, op2(e21,e23) != op2(e22,e23), inference(clausification, [status(esa)], [ax8])). % 43.73/6.94 cnf(c193, plain, op2(e21,e20) != op2(e21,e22), inference(clausification, [status(esa)], [ax8])). % 43.73/6.94 cnf(c195, plain, op2(e21,e21) != op2(e21,e22), inference(clausification, [status(esa)], [ax8])). % 43.73/6.94 cnf(c196, plain, op2(e21,e21) != op2(e21,e23), inference(clausification, [status(esa)], [ax8])). % 43.73/6.94 cnf(c198, plain, op2(e22,e20) != op2(e22,e21), inference(clausification, [status(esa)], [ax8])). % 43.73/6.94 cnf(c210, plain, e10 != e11, inference(clausification, [status(esa)], [ax9])). % 43.73/6.94 cnf(c211, plain, e10 != e12, inference(clausification, [status(esa)], [ax9])). % 43.73/6.94 cnf(c212, plain, e10 != e13, inference(clausification, [status(esa)], [ax9])). % 43.73/6.94 cnf(c213, plain, e11 != e12, inference(clausification, [status(esa)], [ax9])). % 43.73/6.94 cnf(c214, plain, e11 != e13, inference(clausification, [status(esa)], [ax9])). % 43.73/6.94 cnf(c215, plain, e12 != e13, inference(clausification, [status(esa)], [ax9])). % 43.73/6.94 cnf(c216, plain, e20 != e21, inference(clausification, [status(esa)], [ax10])). % 43.73/6.94 cnf(c217, plain, e20 != e22, inference(clausification, [status(esa)], [ax10])). % 43.73/6.94 cnf(c218, plain, e20 != e23, inference(clausification, [status(esa)], [ax10])). % 43.73/6.94 cnf(c219, plain, e21 != e22, inference(clausification, [status(esa)], [ax10])). % 43.73/6.94 cnf(c220, plain, e21 != e23, inference(clausification, [status(esa)], [ax10])). % 43.73/6.94 cnf(c221, plain, e22 != e23, inference(clausification, [status(esa)], [ax10])). % 43.73/6.94 cnf(c246, plain, e10 = op1(e11,op1(e11,op1(e11,e11))), inference(clausification, [status(esa)], [ax14])). % 43.73/6.94 cnf(c247, plain, e12 = op1(e11,op1(e11,e11)), inference(clausification, [status(esa)], [ax14])). % 43.73/6.94 cnf(c248, plain, e13 = op1(e11,e11), inference(clausification, [status(esa)], [ax14])). % 43.73/6.94 cnf(c249, plain, e20 = op2(e21,op2(e21,op2(e21,e21))), inference(clausification, [status(esa)], [ax15])). % 43.73/6.94 cnf(c250, plain, e22 = op2(e21,op2(e21,e21)), inference(clausification, [status(esa)], [ax15])). % 43.73/6.94 cnf(c251, plain, e23 = op2(e21,e21), inference(clausification, [status(esa)], [ax15])). % 43.73/6.94 cnf(c256, plain, h2(e11) = e21, inference(clausification, [status(esa)], [ax17])). % 43.73/6.94 cnf(c257, plain, h2(e10) = op2(e21,op2(e21,op2(e21,e21))), inference(clausification, [status(esa)], [ax17])). % 43.73/6.94 cnf(c258, plain, h2(e12) = op2(e21,op2(e21,e21)), inference(clausification, [status(esa)], [ax17])). % 43.73/6.94 cnf(c259, plain, h2(e13) = op2(e21,e21), inference(clausification, [status(esa)], [ax17])). % 43.73/6.94 cnf(c263, plain, h3(e13) = op2(e22,e22), inference(clausification, [status(esa)], [ax18])). % 43.73/6.94 cnf(c267, plain, h4(e13) = op2(e23,e23), inference(clausification, [status(esa)], [ax19])). % 43.73/6.94 cnf(c275, plain, h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(e13) != e23 | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | ~X0 | ~X1 | h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e10,e11)) != op2(h2(e10),h2(e11)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(op1(e10,e13)) != op2(h2(e10),h2(e13)) | ~X2 | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)), inference(clausification, [status(esa)], [negated_conjecture])). % 43.73/6.94 cnf(c298, plain, X0 | h2(e12) != e22, inference(clausification, [status(esa)], [negated_conjecture])). % 43.73/6.94 cnf(c301, plain, X0 | h2(e11) != e21, inference(clausification, [status(esa)], [negated_conjecture])). % 43.73/6.94 cnf(c304, plain, X0 | h2(e10) != e20, inference(clausification, [status(esa)], [negated_conjecture])). % 43.73/6.94 cnf(d0, plain, e22 = op2(e21,e23), inference(demodulation, [status(thm)], [c250,c251])). % 43.73/6.94 cnf(d1, plain, e20 = op2(e21,op2(e21,e23)), inference(demodulation, [status(thm)], [c249,c251])). % 43.73/6.94 cnf(d2, plain, e20 = op2(e21,e22), inference(demodulation, [status(thm)], [d1,d0])). % 43.73/6.94 cnf(d3, plain, e20 != op2(e23,e22), inference(demodulation, [status(thm)], [c178,d2])). % 43.73/6.94 cnf(d4, plain, e22 != op2(e22,e23), inference(demodulation, [status(thm)], [c183,d0])). % 43.73/6.94 cnf(d5, plain, op2(e22,e23) = e22 | unit2 = e20 | unit2 = e22 | unit2 = e21, inference(superposition, [status(thm)], [c81,c78])). % 43.73/6.94 cnf(d6, plain, e22 != e22 | unit2 = e20 | unit2 = e22 | unit2 = e21, inference(superposition, [status(thm)], [d5,d4])). % 43.73/6.94 cnf(d7, plain, unit2 = e20 | unit2 = e22 | unit2 = e21, inference(equality_resolution, [status(thm)], [d6])). % 43.73/6.94 cnf(d8, plain, op2(e21,e23) = e23 | unit2 = e20 | unit2 = e22, inference(superposition, [status(thm)], [d7,c79])). % 43.73/6.94 cnf(d9, plain, e22 = e23 | unit2 = e20 | unit2 = e22, inference(demodulation, [status(thm)], [d8,d0])). % 43.73/6.94 cnf(d10, plain, unit2 = e20 | unit2 = e22, inference(resolution, [status(thm)], [c221,d9])). % 43.73/6.94 cnf(d11, plain, op2(e20,e22) = e20 | unit2 = e20, inference(superposition, [status(thm)], [d10,c74])). % 43.73/6.94 cnf(d12, plain, op2(e20,e22) != e20, inference(demodulation, [status(thm)], [c174,d2])). % 43.73/6.94 cnf(d13, plain, unit2 = e20, inference(resolution, [status(thm)], [d12,d11])). % 43.73/6.94 cnf(d14, plain, op2(e22,e20) = e22, inference(demodulation, [status(thm)], [c78,d13])). % 43.73/6.94 cnf(d15, plain, e22 != op2(e22,e21), inference(demodulation, [status(thm)], [c198,d14])). % 43.73/6.94 cnf(d16, plain, op2(e20,e21) = e21, inference(demodulation, [status(thm)], [c75,d13])). % 43.73/6.94 cnf(d17, plain, e21 != op2(e22,e21), inference(demodulation, [status(thm)], [c169,d16])). % 43.73/6.94 cnf(d18, plain, e23 != op2(e22,e21), inference(demodulation, [status(thm)], [c171,c251])). % 43.73/6.94 cnf(d19, plain, e23 != e23 | op2(e22,e21) = e20 | op2(e22,e21) = e22 | op2(e22,e21) = e21, inference(superposition, [status(thm)], [c66,d18])). % 43.73/6.94 cnf(d20, plain, op2(e22,e21) = e20 | op2(e22,e21) = e22 | op2(e22,e21) = e21, inference(equality_resolution, [status(thm)], [d19])). % 43.73/6.94 cnf(d21, plain, e21 != e21 | op2(e22,e21) = e20 | op2(e22,e21) = e22, inference(superposition, [status(thm)], [d20,d17])). % 43.73/6.94 cnf(d22, plain, e21 = e20 | op2(e20,e21) = e22 | op2(e20,e21) = e21 | op2(e20,e21) = e23, inference(demodulation, [status(thm)], [c58,d16])). % 43.73/6.94 cnf(d23, plain, e21 = e20 | e21 = e22 | op2(e20,e21) = e21 | op2(e20,e21) = e23, inference(demodulation, [status(thm)], [d22,d16])). % 43.73/6.94 cnf(d24, plain, e21 = e20 | e21 = e22 | e21 = e21 | op2(e20,e21) = e23, inference(demodulation, [status(thm)], [d23,d16])). % 43.73/6.94 cnf(d25, plain, e21 = e20 | e21 = e22 | e21 = e21 | e21 = e23, inference(demodulation, [status(thm)], [d24,d16])). % 43.73/6.94 cnf(d26, plain, e21 = e20 | e21 = e21 | e21 = e23, inference(resolution, [status(thm)], [c219,d25])). % 43.73/6.94 cnf(d27, plain, e21 = e20 | e21 = e21, inference(resolution, [status(thm)], [c220,d26])). % 43.73/6.94 cnf(d28, plain, op2(e21,e20) = e21, inference(demodulation, [status(thm)], [c76,d13])). % 43.73/6.94 cnf(d29, plain, op2(e21,e20) != e20, inference(demodulation, [status(thm)], [c193,d2])). % 43.73/6.94 cnf(d30, plain, e21 != e20, inference(demodulation, [status(thm)], [d29,d28])). % 43.73/6.94 cnf(d31, plain, e21 = e21, inference(resolution, [status(thm)], [d30,d27])). % 43.73/6.94 cnf(d32, plain, op2(e22,e21) = e20 | op2(e22,e21) = e22, inference(resolution, [status(thm)], [d31,d21])). % 43.73/6.94 cnf(d33, plain, e22 != e22 | op2(e22,e21) = e20, inference(superposition, [status(thm)], [d32,d15])). % 43.73/6.94 cnf(d34, plain, op2(e22,e21) = e20, inference(equality_resolution, [status(thm)], [d33])). % 43.73/6.94 cnf(d35, plain, e21 = e22 | op2(e22,e21) = e22 | op2(e21,e21) = e22 | op2(e23,e21) = e22, inference(demodulation, [status(thm)], [c95,d16])). % 43.73/6.94 cnf(d36, plain, e21 = e22 | e20 = e22 | op2(e21,e21) = e22 | op2(e23,e21) = e22, inference(demodulation, [status(thm)], [d35,d34])). % 43.73/6.94 cnf(d37, plain, e21 = e22 | e20 = e22 | e23 = e22 | op2(e23,e21) = e22, inference(demodulation, [status(thm)], [d36,c251])). % 43.73/6.94 cnf(d38, plain, e21 = e22 | e23 = e22 | op2(e23,e21) = e22, inference(resolution, [status(thm)], [c217,d37])). % 43.73/6.94 cnf(d39, plain, op2(e23,e21) = e22 | e23 = e22, inference(resolution, [status(thm)], [c219,d38])). % 43.73/6.94 cnf(d40, plain, e23 != op2(e21,e23), inference(demodulation, [status(thm)], [c196,c251])). % 43.73/6.94 cnf(d41, plain, e23 != e22, inference(demodulation, [status(thm)], [d40,d0])). % 43.73/6.94 cnf(d42, plain, op2(e23,e21) = e22, inference(resolution, [status(thm)], [d41,d39])). % 43.73/6.94 cnf(d43, plain, op2(e23,e20) = e23, inference(demodulation, [status(thm)], [c80,d13])). % 43.73/6.94 cnf(d44, plain, e23 = e20 | op2(e23,e22) = e20 | op2(e23,e21) = e20 | op2(e23,e23) = e20, inference(demodulation, [status(thm)], [c106,d43])). % 43.73/6.94 cnf(d45, plain, e23 = e20 | op2(e23,e22) = e20 | e22 = e20 | op2(e23,e23) = e20, inference(demodulation, [status(thm)], [d44,d42])). % 43.73/6.94 cnf(d46, plain, e23 = e20 | op2(e23,e22) = e20 | e22 = e20 | h4(e13) = e20, inference(demodulation, [status(thm)], [d45,c267])). % 43.73/6.94 cnf(d47, plain, e23 != op2(e21,e22), inference(demodulation, [status(thm)], [c195,c251])). % 43.73/6.94 cnf(d48, plain, e23 != e20, inference(demodulation, [status(thm)], [d47,d2])). % 43.73/6.94 cnf(d49, plain, op2(e23,e22) = e20 | e22 = e20 | h4(e13) = e20, inference(resolution, [status(thm)], [d48,d46])). % 43.73/6.94 cnf(d50, plain, op2(e20,e22) = e22, inference(demodulation, [status(thm)], [c77,d13])). % 43.73/6.94 cnf(d51, plain, e22 != e20, inference(demodulation, [status(thm)], [d12,d50])). % 43.73/6.94 cnf(d52, plain, op2(e23,e22) = e20 | h4(e13) = e20, inference(resolution, [status(thm)], [d51,d49])). % 43.73/6.94 cnf(d53, plain, e20 != e20 | h4(e13) = e20, inference(superposition, [status(thm)], [d52,d3])). % 43.73/6.94 cnf(d54, plain, op2(e21,e22) = e21 | unit2 = e20, inference(superposition, [status(thm)], [d10,c76])). % 43.73/6.94 cnf(d55, plain, e20 = e21 | unit2 = e20, inference(demodulation, [status(thm)], [d54,d2])). % 43.73/6.94 cnf(d56, plain, e20 = e21 | e20 = e20, inference(demodulation, [status(thm)], [d55,d13])). % 43.73/6.94 cnf(d57, plain, e20 = e20, inference(resolution, [status(thm)], [c216,d56])). % 43.73/6.94 cnf(d58, plain, h4(e13) = e20, inference(resolution, [status(thm)], [d57,d53])). % 43.73/6.94 cnf(d59, plain, op2(e20,e23) = e23, inference(demodulation, [status(thm)], [c79,d13])). % 43.73/6.94 cnf(d60, plain, e23 != op2(e22,e23), inference(demodulation, [status(thm)], [c181,d59])). % 43.73/6.94 cnf(d61, plain, e22 = e23 | op2(e22,e22) = e23 | op2(e22,e21) = e23 | op2(e22,e23) = e23, inference(demodulation, [status(thm)], [c104,d14])). % 43.73/6.94 cnf(d62, plain, e22 = e23 | h3(e13) = e23 | op2(e22,e21) = e23 | op2(e22,e23) = e23, inference(demodulation, [status(thm)], [d61,c263])). % 43.73/6.94 cnf(d63, plain, e22 = e23 | h3(e13) = e23 | e20 = e23 | op2(e22,e23) = e23, inference(demodulation, [status(thm)], [d62,d34])). % 43.73/6.94 cnf(d64, plain, e22 = e23 | h3(e13) = e23 | op2(e22,e23) = e23, inference(resolution, [status(thm)], [c218,d63])). % 43.73/6.94 cnf(d65, plain, op2(e22,e23) = e23 | h3(e13) = e23, inference(resolution, [status(thm)], [c221,d64])). % 43.73/6.94 cnf(d66, plain, e23 != e23 | h3(e13) = e23, inference(superposition, [status(thm)], [d65,d60])). % 43.73/6.94 cnf(d67, plain, op2(e20,e20) = e20, inference(demodulation, [status(thm)], [c74,d13])). % 43.73/6.94 cnf(d68, plain, e20 = e23 | op2(e20,e22) = e23 | op2(e20,e21) = e23 | op2(e20,e23) = e23, inference(demodulation, [status(thm)], [c88,d67])). % 43.73/6.94 cnf(d69, plain, e20 = e23 | e22 = e23 | op2(e20,e21) = e23 | op2(e20,e23) = e23, inference(demodulation, [status(thm)], [d68,d50])). % 43.73/6.94 cnf(d70, plain, e20 = e23 | e22 = e23 | e21 = e23 | op2(e20,e23) = e23, inference(demodulation, [status(thm)], [d69,d16])). % 43.73/6.94 cnf(d71, plain, e20 = e23 | e22 = e23 | e21 = e23 | e23 = e23, inference(demodulation, [status(thm)], [d70,d59])). % 43.73/6.94 cnf(d72, plain, e22 = e23 | e21 = e23 | e23 = e23, inference(resolution, [status(thm)], [c218,d71])). % 43.73/6.94 cnf(d73, plain, e22 = e23 | e23 = e23, inference(resolution, [status(thm)], [c220,d72])). % 43.73/6.94 cnf(d74, plain, e23 = e23, inference(resolution, [status(thm)], [c221,d73])). % 43.73/6.94 cnf(d75, plain, h3(e13) = e23, inference(resolution, [status(thm)], [d74,d66])). % 43.73/6.94 cnf(d76, plain, h2(e13) = e23, inference(demodulation, [status(thm)], [c259,c251])). % 43.73/6.94 cnf(d77, plain, e12 = op1(e11,e13), inference(demodulation, [status(thm)], [c247,c248])). % 43.73/6.94 cnf(d78, plain, e12 != op1(e12,e13), inference(demodulation, [status(thm)], [c135,d77])). % 43.73/6.94 cnf(d79, plain, op1(e10,e12) = e10 | unit1 = e10 | unit1 = e11 | unit1 = e13, inference(superposition, [status(thm)], [c24,c17])). % 43.73/6.94 cnf(d80, plain, e10 = op1(e11,op1(e11,e13)), inference(demodulation, [status(thm)], [c246,c248])). % 43.73/6.94 cnf(d81, plain, e10 = op1(e11,e12), inference(demodulation, [status(thm)], [d80,d77])). % 43.73/6.94 cnf(d82, plain, op1(e10,e12) != e10, inference(demodulation, [status(thm)], [c126,d81])). % 43.73/6.94 cnf(d83, plain, unit1 = e10 | unit1 = e11 | unit1 = e13, inference(resolution, [status(thm)], [d82,d79])). % 43.73/6.94 cnf(d84, plain, op1(e12,e13) = e12 | unit1 = e10 | unit1 = e11, inference(superposition, [status(thm)], [d83,c21])). % 43.73/6.94 cnf(d85, plain, e12 != e12 | unit1 = e10 | unit1 = e11, inference(superposition, [status(thm)], [d84,d78])). % 43.73/6.94 cnf(d86, plain, unit1 = e10 | unit1 = e11, inference(equality_resolution, [status(thm)], [d85])). % 43.73/6.94 cnf(d87, plain, op1(e11,e10) = e10 | unit1 = e10, inference(superposition, [status(thm)], [d86,c16])). % 43.73/6.94 cnf(d88, plain, op1(e11,e10) != e10, inference(demodulation, [status(thm)], [c145,d81])). % 43.73/6.94 cnf(d89, plain, unit1 = e10, inference(resolution, [status(thm)], [d88,d87])). % 43.73/6.94 cnf(d90, plain, op1(e10,e13) = e13, inference(demodulation, [status(thm)], [c22,d89])). % 43.73/6.94 cnf(d91, plain, e13 != op1(e12,e13), inference(demodulation, [status(thm)], [c133,d90])). % 43.73/6.94 cnf(d92, plain, e12 != e12 | op1(e12,e13) = e10 | op1(e12,e13) = e11 | op1(e12,e13) = e13, inference(superposition, [status(thm)], [c11,d78])). % 43.73/6.94 cnf(d93, plain, op1(e10,e12) = e12, inference(demodulation, [status(thm)], [c20,d89])). % 43.73/6.94 cnf(d94, plain, op1(e10,e11) = e11, inference(demodulation, [status(thm)], [c18,d89])). % 43.73/6.94 cnf(d95, plain, op1(e10,e10) = e10, inference(demodulation, [status(thm)], [c16,d89])). % 43.73/6.94 cnf(d96, plain, e10 = e12 | op1(e10,e11) = e12 | op1(e10,e13) = e12 | op1(e10,e12) = e12, inference(demodulation, [status(thm)], [c29,d95])). % 43.73/6.94 cnf(d97, plain, e10 = e12 | e11 = e12 | op1(e10,e13) = e12 | op1(e10,e12) = e12, inference(demodulation, [status(thm)], [d96,d94])). % 43.73/6.94 cnf(d98, plain, e10 = e12 | e11 = e12 | e13 = e12 | op1(e10,e12) = e12, inference(demodulation, [status(thm)], [d97,d90])). % 43.73/6.94 cnf(d99, plain, e10 = e12 | e11 = e12 | e13 = e12 | e12 = e12, inference(demodulation, [status(thm)], [d98,d93])). % 43.73/6.94 cnf(d100, plain, e11 = e12 | e13 = e12 | e12 = e12, inference(resolution, [status(thm)], [c211,d99])). % 43.73/6.94 cnf(d101, plain, e13 = e12 | e12 = e12, inference(resolution, [status(thm)], [c213,d100])). % 43.73/6.94 cnf(d102, plain, e13 != op1(e11,e13), inference(demodulation, [status(thm)], [c148,c248])). % 43.73/6.94 cnf(d103, plain, e13 != e12, inference(demodulation, [status(thm)], [d102,d77])). % 43.73/6.94 cnf(d104, plain, e12 = e12, inference(resolution, [status(thm)], [d103,d101])). % 43.73/6.94 cnf(d105, plain, op1(e12,e13) = e10 | op1(e12,e13) = e11 | op1(e12,e13) = e13, inference(resolution, [status(thm)], [d104,d92])). % 43.73/6.94 cnf(d106, plain, e13 != e13 | op1(e12,e13) = e10 | op1(e12,e13) = e11, inference(superposition, [status(thm)], [d105,d91])). % 43.73/6.94 cnf(d107, plain, e10 = e13 | op1(e10,e11) = e13 | op1(e10,e13) = e13 | op1(e10,e12) = e13, inference(demodulation, [status(thm)], [c31,d95])). % 43.73/6.94 cnf(d108, plain, e10 = e13 | e11 = e13 | op1(e10,e13) = e13 | op1(e10,e12) = e13, inference(demodulation, [status(thm)], [d107,d94])). % 43.73/6.94 cnf(d109, plain, e10 = e13 | e11 = e13 | e13 = e13 | op1(e10,e12) = e13, inference(demodulation, [status(thm)], [d108,d90])). % 43.73/6.94 cnf(d110, plain, e10 = e13 | e11 = e13 | e13 = e13 | e12 = e13, inference(demodulation, [status(thm)], [d109,d93])). % 43.73/6.94 cnf(d111, plain, e11 = e13 | e13 = e13 | e12 = e13, inference(resolution, [status(thm)], [c212,d110])). % 43.73/6.94 cnf(d112, plain, e13 = e13 | e12 = e13, inference(resolution, [status(thm)], [c214,d111])). % 43.73/6.94 cnf(d113, plain, e13 = e13, inference(resolution, [status(thm)], [c215,d112])). % 43.73/6.94 cnf(d114, plain, op1(e12,e13) = e10 | op1(e12,e13) = e11, inference(resolution, [status(thm)], [d113,d106])). % 43.73/6.94 cnf(d115, plain, op1(e12,e10) = e12, inference(demodulation, [status(thm)], [c21,d89])). % 43.73/6.94 cnf(d116, plain, e12 != op1(e12,e11), inference(demodulation, [status(thm)], [c150,d115])). % 43.73/6.94 cnf(d117, plain, e11 = e12 | op1(e11,e11) = e12 | op1(e13,e11) = e12 | op1(e12,e11) = e12, inference(demodulation, [status(thm)], [c38,d94])). % 43.73/6.94 cnf(d118, plain, e11 = e12 | e13 = e12 | op1(e13,e11) = e12 | op1(e12,e11) = e12, inference(demodulation, [status(thm)], [d117,c248])). % 43.73/6.94 cnf(d119, plain, e13 = e12 | op1(e13,e11) = e12 | op1(e12,e11) = e12, inference(resolution, [status(thm)], [c213,d118])). % 43.73/6.94 cnf(d120, plain, op1(e13,e11) = e12 | op1(e12,e11) = e12, inference(resolution, [status(thm)], [d103,d119])). % 43.73/6.94 cnf(d121, plain, e12 != e12 | op1(e13,e11) = e12, inference(superposition, [status(thm)], [d120,d116])). % 43.73/6.94 cnf(d122, plain, op1(e13,e11) = e12, inference(resolution, [status(thm)], [d104,d121])). % 43.73/6.94 cnf(d123, plain, e11 = e10 | op1(e11,e11) = e10 | op1(e13,e11) = e10 | op1(e12,e11) = e10, inference(demodulation, [status(thm)], [c34,d94])). % 43.73/6.94 cnf(d124, plain, e11 = e10 | e13 = e10 | op1(e13,e11) = e10 | op1(e12,e11) = e10, inference(demodulation, [status(thm)], [d123,c248])). % 43.73/6.94 cnf(d125, plain, e13 != op1(e11,e12), inference(demodulation, [status(thm)], [c147,c248])). % 43.73/6.94 cnf(d126, plain, e13 != e10, inference(demodulation, [status(thm)], [d125,d81])). % 43.73/6.94 cnf(d127, plain, e11 = e10 | op1(e13,e11) = e10 | op1(e12,e11) = e10, inference(resolution, [status(thm)], [d126,d124])). % 43.73/6.94 cnf(d128, plain, op1(e11,e10) = e11, inference(demodulation, [status(thm)], [c19,d89])). % 43.73/6.94 cnf(d129, plain, e11 != e10, inference(demodulation, [status(thm)], [d88,d128])). % 43.73/6.94 cnf(d130, plain, op1(e13,e11) = e10 | op1(e12,e11) = e10, inference(resolution, [status(thm)], [d129,d127])). % 43.73/6.94 cnf(d131, plain, e12 = e10 | op1(e12,e11) = e10, inference(demodulation, [status(thm)], [d130,d122])). % 43.73/6.94 cnf(d132, plain, e12 != e10, inference(demodulation, [status(thm)], [d82,d93])). % 43.73/6.94 cnf(d133, plain, op1(e12,e11) = e10, inference(resolution, [status(thm)], [d132,d131])). % 43.73/6.94 cnf(d134, plain, e10 != op1(e12,e13), inference(demodulation, [status(thm)], [c154,d133])). % 43.73/6.94 cnf(d135, plain, e11 != op1(e13,e13) | op1(e12,e13) = e10, inference(superposition, [status(thm)], [d114,c137])). % 43.73/6.94 cnf(d136, plain, op1(e13,e10) = e13, inference(demodulation, [status(thm)], [c23,d89])). % 43.73/6.94 cnf(d137, plain, e13 != op1(e13,e13), inference(demodulation, [status(thm)], [c158,d136])). % 43.73/6.94 cnf(d138, plain, e12 != op1(e13,e13), inference(demodulation, [status(thm)], [c136,d77])). % 43.73/6.94 cnf(d139, plain, e12 != e12 | op1(e13,e13) = e10 | op1(e13,e13) = e11 | op1(e13,e13) = e13, inference(superposition, [status(thm)], [c15,d138])). % 43.73/6.94 cnf(d140, plain, op1(e13,e13) = e10 | op1(e13,e13) = e11 | op1(e13,e13) = e13, inference(resolution, [status(thm)], [d104,d139])). % 43.73/6.94 cnf(d141, plain, e13 != e13 | op1(e13,e13) = e10 | op1(e13,e13) = e11, inference(superposition, [status(thm)], [d140,d137])). % 43.73/6.94 cnf(d142, plain, op1(e13,e13) = e10 | op1(e13,e13) = e11, inference(resolution, [status(thm)], [d113,d141])). % 43.73/6.94 cnf(d143, plain, e11 != e11 | op1(e12,e13) = e10 | op1(e13,e13) = e10, inference(superposition, [status(thm)], [d142,d135])). % 43.73/6.94 cnf(d144, plain, op1(e10,e11) != e13, inference(demodulation, [status(thm)], [c120,c248])). % 43.73/6.94 cnf(d145, plain, op1(e10,e11) = e10 | op1(e10,e11) = e11 | op1(e10,e11) = e12, inference(resolution, [status(thm)], [d144,c1])). % 43.73/6.94 cnf(d146, plain, e11 = e10 | op1(e10,e11) = e11 | op1(e10,e11) = e12, inference(demodulation, [status(thm)], [d145,d94])). % 43.73/6.94 cnf(d147, plain, e11 = e10 | e11 = e11 | op1(e10,e11) = e12, inference(demodulation, [status(thm)], [d146,d94])). % 43.73/6.94 cnf(d148, plain, e11 = e10 | e11 = e11 | e11 = e12, inference(demodulation, [status(thm)], [d147,d94])). % 43.73/6.94 cnf(d149, plain, e11 = e10 | e11 = e11, inference(resolution, [status(thm)], [c213,d148])). % 43.73/6.94 cnf(d150, plain, e11 = e11, inference(resolution, [status(thm)], [d129,d149])). % 43.73/6.94 cnf(d151, plain, op1(e13,e13) = e10 | op1(e12,e13) = e10, inference(resolution, [status(thm)], [d150,d143])). % 43.73/6.94 cnf(d152, plain, e10 != e10 | op1(e13,e13) = e10, inference(superposition, [status(thm)], [d151,d134])). % 43.73/6.94 cnf(d153, plain, op1(e11,e12) = e12 | unit1 = e10, inference(superposition, [status(thm)], [d86,c20])). % 43.73/6.94 cnf(d154, plain, e10 = e12 | unit1 = e10, inference(demodulation, [status(thm)], [d153,d81])). % 43.73/6.94 cnf(d155, plain, e10 = e12 | e10 = e10, inference(demodulation, [status(thm)], [d154,d89])). % 43.73/6.94 cnf(d156, plain, e10 = e10, inference(resolution, [status(thm)], [c211,d155])). % 43.73/6.94 cnf(d157, plain, op1(e13,e13) = e10, inference(resolution, [status(thm)], [d156,d152])). % 43.73/6.94 cnf(d158, plain, op1(e12,e13) != e10, inference(demodulation, [status(thm)], [c137,d157])). % 43.73/6.94 cnf(d159, plain, op1(e12,e13) = e11, inference(resolution, [status(thm)], [d158,d114])). % 43.73/6.94 cnf(d160, plain, e12 = e13 | op1(e12,e11) = e13 | op1(e12,e13) = e13 | op1(e12,e12) = e13, inference(demodulation, [status(thm)], [c47,d115])). % 43.73/6.94 cnf(d161, plain, e12 = e13 | e10 = e13 | op1(e12,e13) = e13 | op1(e12,e12) = e13, inference(demodulation, [status(thm)], [d160,d133])). % 43.73/6.94 cnf(d162, plain, e12 = e13 | e10 = e13 | e11 = e13 | op1(e12,e12) = e13, inference(demodulation, [status(thm)], [d161,d159])). % 43.73/6.94 cnf(d163, plain, e12 = e13 | e11 = e13 | op1(e12,e12) = e13, inference(resolution, [status(thm)], [c212,d162])). % 43.73/6.94 cnf(d164, plain, op1(e12,e12) = e13 | e12 = e13, inference(resolution, [status(thm)], [c214,d163])). % 43.73/6.94 cnf(d165, plain, op1(e12,e12) = e13, inference(resolution, [status(thm)], [c215,d164])). % 43.73/6.94 cnf(d166, plain, e12 = e11 | op1(e11,e12) = e11 | op1(e13,e12) = e11 | op1(e12,e12) = e11, inference(demodulation, [status(thm)], [c44,d93])). % 43.73/6.94 cnf(d167, plain, e12 = e11 | e10 = e11 | op1(e13,e12) = e11 | op1(e12,e12) = e11, inference(demodulation, [status(thm)], [d166,d81])). % 43.73/6.94 cnf(d168, plain, e12 = e11 | op1(e13,e12) = e11 | op1(e12,e12) = e11, inference(resolution, [status(thm)], [c210,d167])). % 43.73/6.94 cnf(d169, plain, e12 != e11 | op1(e12,e13) = e10, inference(superposition, [status(thm)], [d114,d78])). % 43.73/6.94 cnf(d170, plain, e12 != e11, inference(resolution, [status(thm)], [d158,d169])). % 43.73/6.94 cnf(d171, plain, op1(e13,e12) = e11 | op1(e12,e12) = e11, inference(resolution, [status(thm)], [d170,d168])). % 43.73/6.94 cnf(d172, plain, op1(e12,e12) != e11, inference(demodulation, [status(thm)], [c155,d159])). % 43.73/6.94 cnf(d173, plain, op1(e13,e12) = e11, inference(resolution, [status(thm)], [d172,d171])). % 43.73/6.94 cnf(d174, plain, h2(e10) = op2(e21,op2(e21,e23)), inference(demodulation, [status(thm)], [c257,c251])). % 43.73/6.94 cnf(d175, plain, h2(e10) = op2(e21,e22), inference(demodulation, [status(thm)], [d174,d0])). % 43.73/6.94 cnf(d176, plain, h2(e10) = e20, inference(demodulation, [status(thm)], [d175,d2])). % 43.73/6.94 cnf(d177, plain, h2(e12) = op2(e21,e23), inference(demodulation, [status(thm)], [c258,c251])). % 43.73/6.94 cnf(d178, plain, h2(e12) = e22, inference(demodulation, [status(thm)], [d177,d0])). % 43.73/6.94 cnf(d179, plain, h2(e10) != op2(h2(e10),h2(e10)) | h2(op1(e10,e11)) != op2(h2(e10),h2(e11)) | h2(op1(e10,e13)) != op2(h2(e10),h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [c275,d95])). % 43.73/6.94 cnf(d180, plain, e20 != op2(h2(e10),h2(e10)) | h2(op1(e10,e11)) != op2(h2(e10),h2(e11)) | h2(op1(e10,e13)) != op2(h2(e10),h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d179,d176])). % 43.73/6.94 cnf(d181, plain, e20 != op2(e20,h2(e10)) | h2(op1(e10,e11)) != op2(h2(e10),h2(e11)) | h2(op1(e10,e13)) != op2(h2(e10),h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d180,d176])). % 43.73/6.94 cnf(d182, plain, e20 != op2(e20,e20) | h2(op1(e10,e11)) != op2(h2(e10),h2(e11)) | h2(op1(e10,e13)) != op2(h2(e10),h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d181,d176])). % 43.73/6.94 cnf(d183, plain, e20 != e20 | h2(op1(e10,e11)) != op2(h2(e10),h2(e11)) | h2(op1(e10,e13)) != op2(h2(e10),h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d182,d67])). % 43.73/6.94 cnf(d184, plain, e20 != e20 | h2(e11) != op2(h2(e10),h2(e11)) | h2(op1(e10,e13)) != op2(h2(e10),h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d183,d94])). % 43.73/6.94 cnf(d185, plain, e20 != e20 | e21 != op2(h2(e10),h2(e11)) | h2(op1(e10,e13)) != op2(h2(e10),h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d184,c256])). % 43.73/6.94 cnf(d186, plain, e20 != e20 | e21 != op2(e20,h2(e11)) | h2(op1(e10,e13)) != op2(h2(e10),h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d185,d176])). % 43.73/6.94 cnf(d187, plain, e20 != e20 | e21 != op2(e20,e21) | h2(op1(e10,e13)) != op2(h2(e10),h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d186,c256])). % 43.73/6.94 cnf(d188, plain, e20 != e20 | e21 != e21 | h2(op1(e10,e13)) != op2(h2(e10),h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d187,d16])). % 43.73/6.94 cnf(d189, plain, e20 != e20 | e21 != e21 | h2(e13) != op2(h2(e10),h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d188,d90])). % 43.73/6.94 cnf(d190, plain, e20 != e20 | e21 != e21 | e23 != op2(h2(e10),h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d189,d76])). % 43.73/6.94 cnf(d191, plain, e20 != e20 | e21 != e21 | e23 != op2(e20,h2(e13)) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d190,d176])). % 43.73/6.94 cnf(d192, plain, e20 != e20 | e21 != e21 | e23 != op2(e20,e23) | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d191,d76])). % 43.73/6.94 cnf(d193, plain, e20 != e20 | e21 != e21 | e23 != e23 | h2(op1(e10,e12)) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d192,d59])). % 43.73/6.94 cnf(d194, plain, e20 != e20 | e21 != e21 | e23 != e23 | h2(e12) != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d193,d93])). % 43.73/6.94 cnf(d195, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != op2(h2(e10),h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d194,d178])). % 43.73/6.94 cnf(d196, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != op2(e20,h2(e12)) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d195,d176])). % 43.73/6.94 cnf(d197, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != op2(e20,e22) | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d196,d178])). % 43.73/6.94 cnf(d198, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | h2(op1(e11,e10)) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d197,d50])). % 43.73/6.94 cnf(d199, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | h2(e11) != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d198,d128])). % 43.73/6.94 cnf(d200, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != op2(h2(e11),h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d199,c256])). % 43.73/6.94 cnf(d201, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != op2(e21,h2(e10)) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d200,c256])). % 43.73/6.94 cnf(d202, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != op2(e21,e20) | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d201,d176])). % 43.73/6.94 cnf(d203, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | h2(op1(e11,e11)) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d202,d28])). % 43.73/6.94 cnf(d204, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | h2(e13) != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d203,c248])). % 43.73/6.94 cnf(d205, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != op2(h2(e11),h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d204,d76])). % 43.73/6.94 cnf(d206, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != op2(e21,h2(e11)) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d205,c256])). % 43.73/6.94 cnf(d207, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != op2(e21,e21) | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d206,c256])). % 43.73/6.94 cnf(d208, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | h2(op1(e11,e13)) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d207,c251])). % 43.73/6.94 cnf(d209, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | h2(e12) != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d208,d77])). % 43.73/6.94 cnf(d210, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != op2(h2(e11),h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d209,d178])). % 43.73/6.94 cnf(d211, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != op2(e21,h2(e13)) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d210,c256])). % 43.73/6.94 cnf(d212, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != op2(e21,e23) | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d211,d76])). % 43.73/6.94 cnf(d213, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | h2(op1(e11,e12)) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d212,d0])). % 43.73/6.94 cnf(d214, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | h2(e10) != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d213,d81])). % 43.73/6.94 cnf(d215, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != op2(h2(e11),h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d214,d176])). % 43.73/6.94 cnf(d216, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != op2(e21,h2(e12)) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d215,c256])). % 43.73/6.94 cnf(d217, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != op2(e21,e22) | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d216,d178])). % 43.73/6.94 cnf(d218, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | h2(op1(e13,e10)) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d217,d2])). % 43.73/6.94 cnf(d219, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | h2(e13) != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d218,d136])). % 43.73/6.94 cnf(d220, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != op2(h2(e13),h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d219,d76])). % 43.73/6.94 cnf(d221, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != op2(e23,h2(e10)) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d220,d76])). % 43.73/6.94 cnf(d222, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != op2(e23,e20) | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d221,d176])). % 43.73/6.94 cnf(d223, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | h2(op1(e13,e11)) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d222,d43])). % 43.73/6.94 cnf(d224, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | h2(e12) != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d223,d122])). % 43.73/6.94 cnf(d225, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(h2(e13),h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d224,d178])). % 43.73/6.94 cnf(d226, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,h2(e11)) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d225,d76])). % 43.73/6.94 cnf(d227, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != op2(h2(e13),h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d226,c256])). % 43.73/6.94 cnf(d228, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != op2(e23,h2(e13)) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d227,d76])). % 43.73/6.94 cnf(d229, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != op2(e23,e23) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d228,d76])). % 43.73/6.94 cnf(d230, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(h2(e13),h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d229,c267])). % 43.73/6.94 cnf(d231, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,h2(e12)) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d230,d76])). % 43.73/6.94 cnf(d232, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | h2(op1(e12,e10)) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d231,d178])). % 43.73/6.94 cnf(d233, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | h2(e12) != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d232,d115])). % 43.73/6.94 cnf(d234, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != op2(h2(e12),h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d233,d178])). % 43.73/6.94 cnf(d235, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != op2(e22,h2(e10)) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d234,d178])). % 43.73/6.94 cnf(d236, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != op2(e22,e20) | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d235,d176])). % 43.73/6.94 cnf(d237, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != e22 | h2(op1(e12,e11)) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d236,d14])). % 43.73/6.94 cnf(d238, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != e22 | h2(e10) != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d237,d133])). % 43.73/6.94 cnf(d239, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != e22 | e20 != op2(h2(e12),h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d238,d176])). % 43.73/6.94 cnf(d240, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != e22 | e20 != op2(e22,h2(e11)) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d239,d178])). % 43.73/6.94 cnf(d241, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != e22 | e20 != op2(e22,e21) | h2(op1(e12,e13)) != op2(h2(e12),h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d240,c256])). % 43.73/6.94 cnf(d242, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != e22 | e20 != op2(e22,e21) | h2(op1(e12,e13)) != op2(e22,h2(e13)) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d241,d178])). % 43.73/6.94 cnf(d243, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != e22 | e20 != op2(e22,e21) | h2(op1(e12,e13)) != op2(e22,e23) | h2(op1(e12,e12)) != op2(h2(e12),h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d242,d76])). % 43.73/6.94 cnf(d244, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != e22 | e20 != op2(e22,e21) | h2(op1(e12,e13)) != op2(e22,e23) | h2(op1(e12,e12)) != op2(e22,h2(e12)) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d243,d178])). % 43.73/6.94 cnf(d245, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != e22 | e20 != op2(e22,e21) | h2(op1(e12,e13)) != op2(e22,e23) | h2(op1(e12,e12)) != op2(e22,e22) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d244,d178])). % 43.73/6.94 cnf(d246, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != e22 | e20 != op2(e22,e21) | h2(op1(e12,e13)) != op2(e22,e23) | h2(op1(e12,e12)) != h3(e13) | h2(e13) != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d245,c263])). % 43.73/6.94 cnf(d247, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != e22 | e20 != op2(e22,e21) | h2(op1(e12,e13)) != op2(e22,e23) | h2(op1(e12,e12)) != h3(e13) | e23 != e23 | ~'Ts4' | ~'Ts5' | ~'Ts3', inference(demodulation, [status(thm)], [d246,d76])). % 43.73/6.94 cnf(d248, plain, 'Ts4', inference(resolution, [status(thm)], [c256,c301])). % 43.73/6.94 cnf(d249, plain, e20 != e20 | e21 != e21 | e23 != e23 | e22 != e22 | e21 != e21 | e23 != e23 | e22 != e22 | e20 != e20 | e23 != e23 | e22 != op2(e23,e21) | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | e22 != e22 | e20 != op2(e22,e21) | h2(op1(e12,e13)) != op2(e22,e23) | h2(op1(e12,e12)) != h3(e13) | e23 != e23 | ~'Ts5' | ~'Ts3', inference(resolution, [status(thm)], [d248,d247])). % 43.73/6.94 cnf(d250, plain, 'Ts5', inference(resolution, [status(thm)], [d176,c304])). % 43.73/6.94 cnf(d251, plain, e20 != op2(e22,e21) | e20 != e20 | e22 != op2(e23,e21) | e22 != e22 | e21 != e21 | e23 != e23 | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | h2(op1(e12,e13)) != op2(e22,e23) | h2(op1(e12,e12)) != h3(e13) | ~'Ts3', inference(resolution, [status(thm)], [d250,d249])). % 43.73/6.94 cnf(d252, plain, e20 != op2(e22,e21) | e22 != op2(e23,e21) | e22 != e22 | e21 != e21 | e23 != e23 | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | h2(op1(e12,e13)) != op2(e22,e23) | h2(op1(e12,e12)) != h3(e13) | ~'Ts3', inference(resolution, [status(thm)], [d57,d251])). % 43.73/6.94 cnf(d253, plain, 'Ts3', inference(resolution, [status(thm)], [d178,c298])). % 43.73/6.94 cnf(d254, plain, e20 != op2(e22,e21) | e22 != op2(e23,e21) | e22 != e22 | e21 != e21 | e23 != e23 | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | h2(op1(e12,e13)) != op2(e22,e23) | h2(op1(e12,e12)) != h3(e13), inference(resolution, [status(thm)], [d253,d252])). % 43.73/6.94 cnf(d255, plain, h2(e11) != op2(e22,e23) | e20 != op2(e22,e21) | e22 != op2(e23,e21) | e22 != e22 | e21 != e21 | e23 != e23 | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | h2(op1(e12,e12)) != h3(e13) | op1(e12,e13) = e10, inference(superposition, [status(thm)], [d114,d254])). % 43.73/6.94 cnf(d256, plain, op1(e12,e13) = e10 | e20 != op2(e22,e21) | e22 != op2(e23,e21) | e22 != e22 | e21 != e21 | e23 != e23 | h2(op1(e13,e13)) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | h2(op1(e12,e12)) != h3(e13) | e21 != op2(e22,e23), inference(demodulation, [status(thm)], [d255,c256])). % 43.73/6.94 cnf(d257, plain, op1(e12,e13) = e10 | e20 != op2(e22,e21) | e22 != op2(e23,e21) | e22 != e22 | e21 != e21 | e23 != e23 | h2(e10) != h4(e13) | h2(op1(e13,e12)) != op2(e23,e22) | h2(op1(e12,e12)) != h3(e13) | e21 != op2(e22,e23), inference(demodulation, [status(thm)], [d256,d157])). % 43.73/6.94 cnf(d258, plain, op1(e12,e13) = e10 | e20 != op2(e22,e21) | e22 != op2(e23,e21) | e22 != e22 | e21 != op2(e22,e23) | e21 != e21 | e23 != e23 | h2(op1(e13,e12)) != op2(e23,e22) | h2(op1(e12,e12)) != h3(e13) | e20 != h4(e13), inference(demodulation, [status(thm)], [d257,d176])). % 43.73/6.94 cnf(d259, plain, e20 != op2(e22,e21) | e22 != op2(e23,e21) | e22 != e22 | e21 != op2(e22,e23) | e21 != e21 | e23 != e23 | h2(op1(e13,e12)) != op2(e23,e22) | h2(op1(e12,e12)) != h3(e13) | e20 != h4(e13), inference(resolution, [status(thm)], [d158,d258])). % 43.73/6.94 cnf(d260, plain, e20 != op2(e22,e21) | e20 != h4(e13) | e22 != op2(e23,e21) | e22 != e22 | e21 != op2(e22,e23) | e21 != e21 | e23 != e23 | h2(e11) != op2(e23,e22) | h2(op1(e12,e12)) != h3(e13), inference(demodulation, [status(thm)], [d259,d173])). % 43.73/6.94 cnf(d261, plain, e20 != op2(e22,e21) | e20 != h4(e13) | e22 != op2(e23,e21) | e22 != e22 | e21 != op2(e22,e23) | e21 != e21 | e23 != e23 | h2(op1(e12,e12)) != h3(e13) | e21 != op2(e23,e22), inference(demodulation, [status(thm)], [d260,c256])). % 43.73/6.94 cnf(d262, plain, e20 != op2(e22,e21) | e20 != h4(e13) | e22 != op2(e23,e21) | e22 != e22 | e21 != op2(e22,e23) | e21 != e21 | e23 != e23 | h2(e13) != h3(e13) | e21 != op2(e23,e22), inference(demodulation, [status(thm)], [d261,d165])). % 43.73/6.94 cnf(d263, plain, e20 != op2(e22,e21) | e20 != h4(e13) | e22 != op2(e23,e21) | e22 != e22 | e21 != op2(e22,e23) | e21 != op2(e23,e22) | e21 != e21 | e23 != e23 | e23 != h3(e13), inference(demodulation, [status(thm)], [d262,d76])). % 43.73/6.94 cnf(d264, plain, e20 != op2(e22,e21) | e20 != h4(e13) | e22 != op2(e23,e21) | e22 != e22 | e21 != op2(e22,e23) | e21 != op2(e23,e22) | e23 != e23 | e23 != h3(e13), inference(resolution, [status(thm)], [d31,d263])). % 43.73/6.94 cnf(d265, plain, e20 != e20 | e20 != h4(e13) | e22 != op2(e23,e21) | e22 != e22 | e21 != op2(e22,e23) | e21 != op2(e23,e22) | e23 != e23 | e23 != h3(e13), inference(demodulation, [status(thm)], [d264,d34])). % 43.73/6.94 cnf(d266, plain, e20 != h4(e13) | e22 != op2(e23,e21) | e22 != e22 | e21 != op2(e22,e23) | e21 != op2(e23,e22) | e23 != e23 | e23 != h3(e13), inference(resolution, [status(thm)], [d57,d265])). % 43.73/6.94 cnf(d267, plain, e20 = e22 | op2(e20,e22) = e22 | op2(e20,e21) = e22 | op2(e20,e23) = e22, inference(demodulation, [status(thm)], [c86,d67])). % 43.73/6.94 cnf(d268, plain, e20 = e22 | e22 = e22 | op2(e20,e21) = e22 | op2(e20,e23) = e22, inference(demodulation, [status(thm)], [d267,d50])). % 43.73/6.94 cnf(d269, plain, e20 = e22 | e22 = e22 | e21 = e22 | op2(e20,e23) = e22, inference(demodulation, [status(thm)], [d268,d16])). % 43.73/6.94 cnf(d270, plain, e20 = e22 | e22 = e22 | e21 = e22 | e23 = e22, inference(demodulation, [status(thm)], [d269,d59])). % 43.73/6.94 cnf(d271, plain, e22 = e22 | e21 = e22 | e23 = e22, inference(resolution, [status(thm)], [c217,d270])). % 43.73/6.94 cnf(d272, plain, e22 = e22 | e23 = e22, inference(resolution, [status(thm)], [c219,d271])). % 43.73/6.94 cnf(d273, plain, e22 = e22, inference(resolution, [status(thm)], [d41,d272])). % 43.73/6.94 cnf(d274, plain, e20 != h4(e13) | e22 != op2(e23,e21) | e21 != op2(e22,e23) | e21 != op2(e23,e22) | e23 != e23 | e23 != h3(e13), inference(resolution, [status(thm)], [d273,d266])). % 43.73/6.94 cnf(d275, plain, e20 != h4(e13) | e22 != op2(e23,e21) | e21 != op2(e22,e23) | e21 != op2(e23,e22) | e23 != h3(e13), inference(resolution, [status(thm)], [d74,d274])). % 43.73/6.94 cnf(d276, plain, e20 != h4(e13) | e22 != e22 | e21 != op2(e22,e23) | e21 != op2(e23,e22) | e23 != h3(e13), inference(demodulation, [status(thm)], [d275,d42])). % 43.73/6.94 cnf(d277, plain, e20 != h4(e13) | e21 != op2(e22,e23) | e21 != op2(e23,e22) | e23 != h3(e13), inference(resolution, [status(thm)], [d273,d276])). % 43.73/6.94 cnf(d278, plain, e22 = e21 | op2(e22,e22) = e21 | op2(e21,e22) = e21 | op2(e23,e22) = e21, inference(demodulation, [status(thm)], [c101,d50])). % 43.73/6.94 cnf(d279, plain, e22 = e21 | h3(e13) = e21 | op2(e21,e22) = e21 | op2(e23,e22) = e21, inference(demodulation, [status(thm)], [d278,c263])). % 43.73/6.94 cnf(d280, plain, e22 = e21 | h3(e13) = e21 | e20 = e21 | op2(e23,e22) = e21, inference(demodulation, [status(thm)], [d279,d2])). % 43.73/6.94 cnf(d281, plain, e22 = e21 | h3(e13) = e21 | op2(e23,e22) = e21, inference(resolution, [status(thm)], [c216,d280])). % 43.73/6.94 cnf(d282, plain, e21 != e21 | e20 != h4(e13) | e21 != op2(e22,e23) | e23 != h3(e13) | e22 = e21 | h3(e13) = e21, inference(superposition, [status(thm)], [d281,d277])). % 43.73/6.94 cnf(d283, plain, e20 != h4(e13) | e22 = e21 | e21 != op2(e22,e23) | e23 != h3(e13) | h3(e13) = e21, inference(resolution, [status(thm)], [d31,d282])). % 43.73/6.94 cnf(d284, plain, e22 = e21 | op2(e22,e22) = e21 | op2(e22,e21) = e21 | op2(e22,e23) = e21, inference(demodulation, [status(thm)], [c100,d14])). % 43.73/6.94 cnf(d285, plain, e22 = e21 | h3(e13) = e21 | op2(e22,e21) = e21 | op2(e22,e23) = e21, inference(demodulation, [status(thm)], [d284,c263])). % 43.73/6.94 cnf(d286, plain, e22 = e21 | h3(e13) = e21 | e20 = e21 | op2(e22,e23) = e21, inference(demodulation, [status(thm)], [d285,d34])). % 43.73/6.94 cnf(d287, plain, e22 = e21 | h3(e13) = e21 | op2(e22,e23) = e21, inference(resolution, [status(thm)], [c216,d286])). % 43.73/6.94 cnf(d288, plain, e21 != e21 | e20 != h4(e13) | e22 = e21 | e23 != h3(e13) | h3(e13) = e21 | e22 = e21 | h3(e13) = e21, inference(superposition, [status(thm)], [d287,d283])). % 43.73/6.94 cnf(d289, plain, e20 != h4(e13) | e22 = e21 | e23 != h3(e13) | h3(e13) = e21, inference(resolution, [status(thm)], [d31,d288])). % 43.73/6.94 cnf(d290, plain, e20 != h4(e13) | e22 = e21 | e23 != e23 | h3(e13) = e21, inference(demodulation, [status(thm)], [d289,d75])). % 43.73/6.94 cnf(d291, plain, e20 != h4(e13) | e22 = e21 | e23 != e23 | e23 = e21, inference(demodulation, [status(thm)], [d290,d75])). % 43.73/6.94 cnf(d292, plain, e20 != h4(e13) | e22 = e21 | e23 = e21, inference(resolution, [status(thm)], [d74,d291])). % 43.73/6.94 cnf(d293, plain, e20 != e20 | e22 = e21 | e23 = e21, inference(demodulation, [status(thm)], [d292,d58])). % 43.73/6.94 cnf(d294, plain, e22 = e21 | e23 = e21, inference(resolution, [status(thm)], [d57,d293])). % 43.73/6.94 cnf(d295, plain, e21 != e21 | e22 = e21, inference(superposition, [status(thm)], [d294,c220])). % 43.73/6.94 cnf(d296, plain, e22 = e21, inference(resolution, [status(thm)], [d31,d295])). % 43.73/6.94 cnf(d297, plain, e21 != e21, inference(demodulation, [status(thm)], [c219,d296])). % 43.73/6.94 cnf(d298, plain, $false, inference(resolution, [status(thm)], [d31,d297])). % 43.73/6.94 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------