%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG056+1 : TPTP v9.3.1. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n001.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:19 AM UTC 2026 % Result : Theorem 160.72s 24.13s % Output : CNFRefutation 160.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : ALG056+1 : TPTP v9.3.1. Released v2.7.0. % 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.45 % Computer : n001.cluster.edu % 0.19/0.45 % Model : x86_64 x86_64 % 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.19/0.45 % Memory : 8046.5625MB % 0.19/0.45 % OS : Linux 6.8.0-71-generic % 0.19/0.46 % CPULimit : 300 % 0.19/0.46 % WCLimit : 300 % 0.19/0.46 % DateTime : Sat Sep 26 21:07:59 UTC 2026 % 0.19/0.46 % CPUTime : % 0.19/0.46 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 160.72/24.13 % SZS status Theorem for theBenchmark.p % 160.72/24.13 % SZS output start CNFRefutation for theBenchmark.p % 160.72/24.13 fof(ax1, axiom, ((op(e0,e0) = e0 | (op(e0,e0) = e1 | (op(e0,e0) = e2 | (op(e0,e0) = e3 | op(e0,e0) = e4)))) & ((op(e0,e1) = e0 | (op(e0,e1) = e1 | (op(e0,e1) = e2 | (op(e0,e1) = e3 | op(e0,e1) = e4)))) & ((op(e0,e2) = e0 | (op(e0,e2) = e1 | (op(e0,e2) = e2 | (op(e0,e2) = e3 | op(e0,e2) = e4)))) & ((op(e0,e3) = e0 | (op(e0,e3) = e1 | (op(e0,e3) = e2 | (op(e0,e3) = e3 | op(e0,e3) = e4)))) & ((op(e0,e4) = e0 | (op(e0,e4) = e1 | (op(e0,e4) = e2 | (op(e0,e4) = e3 | op(e0,e4) = e4)))) & ((op(e1,e0) = e0 | (op(e1,e0) = e1 | (op(e1,e0) = e2 | (op(e1,e0) = e3 | op(e1,e0) = e4)))) & ((op(e1,e1) = e0 | (op(e1,e1) = e1 | (op(e1,e1) = e2 | (op(e1,e1) = e3 | op(e1,e1) = e4)))) & ((op(e1,e2) = e0 | (op(e1,e2) = e1 | (op(e1,e2) = e2 | (op(e1,e2) = e3 | op(e1,e2) = e4)))) & ((op(e1,e3) = e0 | (op(e1,e3) = e1 | (op(e1,e3) = e2 | (op(e1,e3) = e3 | op(e1,e3) = e4)))) & ((op(e1,e4) = e0 | (op(e1,e4) = e1 | (op(e1,e4) = e2 | (op(e1,e4) = e3 | op(e1,e4) = e4)))) & ((op(e2,e0) = e0 | (op(e2,e0) = e1 | (op(e2,e0) = e2 | (op(e2,e0) = e3 | op(e2,e0) = e4)))) & ((op(e2,e1) = e0 | (op(e2,e1) = e1 | (op(e2,e1) = e2 | (op(e2,e1) = e3 | op(e2,e1) = e4)))) & ((op(e2,e2) = e0 | (op(e2,e2) = e1 | (op(e2,e2) = e2 | (op(e2,e2) = e3 | op(e2,e2) = e4)))) & ((op(e2,e3) = e0 | (op(e2,e3) = e1 | (op(e2,e3) = e2 | (op(e2,e3) = e3 | op(e2,e3) = e4)))) & ((op(e2,e4) = e0 | (op(e2,e4) = e1 | (op(e2,e4) = e2 | (op(e2,e4) = e3 | op(e2,e4) = e4)))) & ((op(e3,e0) = e0 | (op(e3,e0) = e1 | (op(e3,e0) = e2 | (op(e3,e0) = e3 | op(e3,e0) = e4)))) & ((op(e3,e1) = e0 | (op(e3,e1) = e1 | (op(e3,e1) = e2 | (op(e3,e1) = e3 | op(e3,e1) = e4)))) & ((op(e3,e2) = e0 | (op(e3,e2) = e1 | (op(e3,e2) = e2 | (op(e3,e2) = e3 | op(e3,e2) = e4)))) & ((op(e3,e3) = e0 | (op(e3,e3) = e1 | (op(e3,e3) = e2 | (op(e3,e3) = e3 | op(e3,e3) = e4)))) & ((op(e3,e4) = e0 | (op(e3,e4) = e1 | (op(e3,e4) = e2 | (op(e3,e4) = e3 | op(e3,e4) = e4)))) & ((op(e4,e0) = e0 | (op(e4,e0) = e1 | (op(e4,e0) = e2 | (op(e4,e0) = e3 | op(e4,e0) = e4)))) & ((op(e4,e1) = e0 | (op(e4,e1) = e1 | (op(e4,e1) = e2 | (op(e4,e1) = e3 | op(e4,e1) = e4)))) & ((op(e4,e2) = e0 | (op(e4,e2) = e1 | (op(e4,e2) = e2 | (op(e4,e2) = e3 | op(e4,e2) = e4)))) & ((op(e4,e3) = e0 | (op(e4,e3) = e1 | (op(e4,e3) = e2 | (op(e4,e3) = e3 | op(e4,e3) = e4)))) & (op(e4,e4) = e0 | (op(e4,e4) = e1 | (op(e4,e4) = e2 | (op(e4,e4) = e3 | op(e4,e4) = e4))))))))))))))))))))))))))))). % 160.72/24.13 fof(ax2, axiom, (op(unit,e0) = e0 & (op(e0,unit) = e0 & (op(unit,e1) = e1 & (op(e1,unit) = e1 & (op(unit,e2) = e2 & (op(e2,unit) = e2 & (op(unit,e3) = e3 & (op(e3,unit) = e3 & (op(unit,e4) = e4 & (op(e4,unit) = e4 & (unit = e0 | (unit = e1 | (unit = e2 | (unit = e3 | unit = e4))))))))))))))). % 160.72/24.13 fof(ax3, axiom, ((op(e0,e0) = e0 | (op(e0,e1) = e0 | (op(e0,e2) = e0 | (op(e0,e3) = e0 | op(e0,e4) = e0)))) & ((op(e0,e0) = e0 | (op(e1,e0) = e0 | (op(e2,e0) = e0 | (op(e3,e0) = e0 | op(e4,e0) = e0)))) & ((op(e0,e0) = e1 | (op(e0,e1) = e1 | (op(e0,e2) = e1 | (op(e0,e3) = e1 | op(e0,e4) = e1)))) & ((op(e0,e0) = e1 | (op(e1,e0) = e1 | (op(e2,e0) = e1 | (op(e3,e0) = e1 | op(e4,e0) = e1)))) & ((op(e0,e0) = e2 | (op(e0,e1) = e2 | (op(e0,e2) = e2 | (op(e0,e3) = e2 | op(e0,e4) = e2)))) & ((op(e0,e0) = e2 | (op(e1,e0) = e2 | (op(e2,e0) = e2 | (op(e3,e0) = e2 | op(e4,e0) = e2)))) & ((op(e0,e0) = e3 | (op(e0,e1) = e3 | (op(e0,e2) = e3 | (op(e0,e3) = e3 | op(e0,e4) = e3)))) & ((op(e0,e0) = e3 | (op(e1,e0) = e3 | (op(e2,e0) = e3 | (op(e3,e0) = e3 | op(e4,e0) = e3)))) & ((op(e0,e0) = e4 | (op(e0,e1) = e4 | (op(e0,e2) = e4 | (op(e0,e3) = e4 | op(e0,e4) = e4)))) & ((op(e0,e0) = e4 | (op(e1,e0) = e4 | (op(e2,e0) = e4 | (op(e3,e0) = e4 | op(e4,e0) = e4)))) & ((op(e1,e0) = e0 | (op(e1,e1) = e0 | (op(e1,e2) = e0 | (op(e1,e3) = e0 | op(e1,e4) = e0)))) & ((op(e0,e1) = e0 | (op(e1,e1) = e0 | (op(e2,e1) = e0 | (op(e3,e1) = e0 | op(e4,e1) = e0)))) & ((op(e1,e0) = e1 | (op(e1,e1) = e1 | (op(e1,e2) = e1 | (op(e1,e3) = e1 | op(e1,e4) = e1)))) & ((op(e0,e1) = e1 | (op(e1,e1) = e1 | (op(e2,e1) = e1 | (op(e3,e1) = e1 | op(e4,e1) = e1)))) & ((op(e1,e0) = e2 | (op(e1,e1) = e2 | (op(e1,e2) = e2 | (op(e1,e3) = e2 | op(e1,e4) = e2)))) & ((op(e0,e1) = e2 | (op(e1,e1) = e2 | (op(e2,e1) = e2 | (op(e3,e1) = e2 | op(e4,e1) = e2)))) & ((op(e1,e0) = e3 | (op(e1,e1) = e3 | (op(e1,e2) = e3 | (op(e1,e3) = e3 | op(e1,e4) = e3)))) & ((op(e0,e1) = e3 | (op(e1,e1) = e3 | (op(e2,e1) = e3 | (op(e3,e1) = e3 | op(e4,e1) = e3)))) & ((op(e1,e0) = e4 | (op(e1,e1) = e4 | (op(e1,e2) = e4 | (op(e1,e3) = e4 | op(e1,e4) = e4)))) & ((op(e0,e1) = e4 | (op(e1,e1) = e4 | (op(e2,e1) = e4 | (op(e3,e1) = e4 | op(e4,e1) = e4)))) & ((op(e2,e0) = e0 | (op(e2,e1) = e0 | (op(e2,e2) = e0 | (op(e2,e3) = e0 | op(e2,e4) = e0)))) & ((op(e0,e2) = e0 | (op(e1,e2) = e0 | (op(e2,e2) = e0 | (op(e3,e2) = e0 | op(e4,e2) = e0)))) & ((op(e2,e0) = e1 | (op(e2,e1) = e1 | (op(e2,e2) = e1 | (op(e2,e3) = e1 | op(e2,e4) = e1)))) & ((op(e0,e2) = e1 | (op(e1,e2) = e1 | (op(e2,e2) = e1 | (op(e3,e2) = e1 | op(e4,e2) = e1)))) & ((op(e2,e0) = e2 | (op(e2,e1) = e2 | (op(e2,e2) = e2 | (op(e2,e3) = e2 | op(e2,e4) = e2)))) & ((op(e0,e2) = e2 | (op(e1,e2) = e2 | (op(e2,e2) = e2 | (op(e3,e2) = e2 | op(e4,e2) = e2)))) & ((op(e2,e0) = e3 | (op(e2,e1) = e3 | (op(e2,e2) = e3 | (op(e2,e3) = e3 | op(e2,e4) = e3)))) & ((op(e0,e2) = e3 | (op(e1,e2) = e3 | (op(e2,e2) = e3 | (op(e3,e2) = e3 | op(e4,e2) = e3)))) & ((op(e2,e0) = e4 | (op(e2,e1) = e4 | (op(e2,e2) = e4 | (op(e2,e3) = e4 | op(e2,e4) = e4)))) & ((op(e0,e2) = e4 | (op(e1,e2) = e4 | (op(e2,e2) = e4 | (op(e3,e2) = e4 | op(e4,e2) = e4)))) & ((op(e3,e0) = e0 | (op(e3,e1) = e0 | (op(e3,e2) = e0 | (op(e3,e3) = e0 | op(e3,e4) = e0)))) & ((op(e0,e3) = e0 | (op(e1,e3) = e0 | (op(e2,e3) = e0 | (op(e3,e3) = e0 | op(e4,e3) = e0)))) & ((op(e3,e0) = e1 | (op(e3,e1) = e1 | (op(e3,e2) = e1 | (op(e3,e3) = e1 | op(e3,e4) = e1)))) & ((op(e0,e3) = e1 | (op(e1,e3) = e1 | (op(e2,e3) = e1 | (op(e3,e3) = e1 | op(e4,e3) = e1)))) & ((op(e3,e0) = e2 | (op(e3,e1) = e2 | (op(e3,e2) = e2 | (op(e3,e3) = e2 | op(e3,e4) = e2)))) & ((op(e0,e3) = e2 | (op(e1,e3) = e2 | (op(e2,e3) = e2 | (op(e3,e3) = e2 | op(e4,e3) = e2)))) & ((op(e3,e0) = e3 | (op(e3,e1) = e3 | (op(e3,e2) = e3 | (op(e3,e3) = e3 | op(e3,e4) = e3)))) & ((op(e0,e3) = e3 | (op(e1,e3) = e3 | (op(e2,e3) = e3 | (op(e3,e3) = e3 | op(e4,e3) = e3)))) & ((op(e3,e0) = e4 | (op(e3,e1) = e4 | (op(e3,e2) = e4 | (op(e3,e3) = e4 | op(e3,e4) = e4)))) & ((op(e0,e3) = e4 | (op(e1,e3) = e4 | (op(e2,e3) = e4 | (op(e3,e3) = e4 | op(e4,e3) = e4)))) & ((op(e4,e0) = e0 | (op(e4,e1) = e0 | (op(e4,e2) = e0 | (op(e4,e3) = e0 | op(e4,e4) = e0)))) & ((op(e0,e4) = e0 | (op(e1,e4) = e0 | (op(e2,e4) = e0 | (op(e3,e4) = e0 | op(e4,e4) = e0)))) & ((op(e4,e0) = e1 | (op(e4,e1) = e1 | (op(e4,e2) = e1 | (op(e4,e3) = e1 | op(e4,e4) = e1)))) & ((op(e0,e4) = e1 | (op(e1,e4) = e1 | (op(e2,e4) = e1 | (op(e3,e4) = e1 | op(e4,e4) = e1)))) & ((op(e4,e0) = e2 | (op(e4,e1) = e2 | (op(e4,e2) = e2 | (op(e4,e3) = e2 | op(e4,e4) = e2)))) & ((op(e0,e4) = e2 | (op(e1,e4) = e2 | (op(e2,e4) = e2 | (op(e3,e4) = e2 | op(e4,e4) = e2)))) & ((op(e4,e0) = e3 | (op(e4,e1) = e3 | (op(e4,e2) = e3 | (op(e4,e3) = e3 | op(e4,e4) = e3)))) & ((op(e0,e4) = e3 | (op(e1,e4) = e3 | (op(e2,e4) = e3 | (op(e3,e4) = e3 | op(e4,e4) = e3)))) & ((op(e4,e0) = e4 | (op(e4,e1) = e4 | (op(e4,e2) = e4 | (op(e4,e3) = e4 | op(e4,e4) = e4)))) & (op(e0,e4) = e4 | (op(e1,e4) = e4 | (op(e2,e4) = e4 | (op(e3,e4) = e4 | op(e4,e4) = e4)))))))))))))))))))))))))))))))))))))))))))))))))))))). % 160.72/24.13 fof(ax4, axiom, (op(e0,e0) != op(e1,e0) & (op(e0,e0) != op(e2,e0) & (op(e0,e0) != op(e3,e0) & (op(e0,e0) != op(e4,e0) & (op(e1,e0) != op(e2,e0) & (op(e1,e0) != op(e3,e0) & (op(e1,e0) != op(e4,e0) & (op(e2,e0) != op(e3,e0) & (op(e2,e0) != op(e4,e0) & (op(e3,e0) != op(e4,e0) & (op(e0,e1) != op(e1,e1) & (op(e0,e1) != op(e2,e1) & (op(e0,e1) != op(e3,e1) & (op(e0,e1) != op(e4,e1) & (op(e1,e1) != op(e2,e1) & (op(e1,e1) != op(e3,e1) & (op(e1,e1) != op(e4,e1) & (op(e2,e1) != op(e3,e1) & (op(e2,e1) != op(e4,e1) & (op(e3,e1) != op(e4,e1) & (op(e0,e2) != op(e1,e2) & (op(e0,e2) != op(e2,e2) & (op(e0,e2) != op(e3,e2) & (op(e0,e2) != op(e4,e2) & (op(e1,e2) != op(e2,e2) & (op(e1,e2) != op(e3,e2) & (op(e1,e2) != op(e4,e2) & (op(e2,e2) != op(e3,e2) & (op(e2,e2) != op(e4,e2) & (op(e3,e2) != op(e4,e2) & (op(e0,e3) != op(e1,e3) & (op(e0,e3) != op(e2,e3) & (op(e0,e3) != op(e3,e3) & (op(e0,e3) != op(e4,e3) & (op(e1,e3) != op(e2,e3) & (op(e1,e3) != op(e3,e3) & (op(e1,e3) != op(e4,e3) & (op(e2,e3) != op(e3,e3) & (op(e2,e3) != op(e4,e3) & (op(e3,e3) != op(e4,e3) & (op(e0,e4) != op(e1,e4) & (op(e0,e4) != op(e2,e4) & (op(e0,e4) != op(e3,e4) & (op(e0,e4) != op(e4,e4) & (op(e1,e4) != op(e2,e4) & (op(e1,e4) != op(e3,e4) & (op(e1,e4) != op(e4,e4) & (op(e2,e4) != op(e3,e4) & (op(e2,e4) != op(e4,e4) & (op(e3,e4) != op(e4,e4) & (op(e0,e0) != op(e0,e1) & (op(e0,e0) != op(e0,e2) & (op(e0,e0) != op(e0,e3) & (op(e0,e0) != op(e0,e4) & (op(e0,e1) != op(e0,e2) & (op(e0,e1) != op(e0,e3) & (op(e0,e1) != op(e0,e4) & (op(e0,e2) != op(e0,e3) & (op(e0,e2) != op(e0,e4) & (op(e0,e3) != op(e0,e4) & (op(e1,e0) != op(e1,e1) & (op(e1,e0) != op(e1,e2) & (op(e1,e0) != op(e1,e3) & (op(e1,e0) != op(e1,e4) & (op(e1,e1) != op(e1,e2) & (op(e1,e1) != op(e1,e3) & (op(e1,e1) != op(e1,e4) & (op(e1,e2) != op(e1,e3) & (op(e1,e2) != op(e1,e4) & (op(e1,e3) != op(e1,e4) & (op(e2,e0) != op(e2,e1) & (op(e2,e0) != op(e2,e2) & (op(e2,e0) != op(e2,e3) & (op(e2,e0) != op(e2,e4) & (op(e2,e1) != op(e2,e2) & (op(e2,e1) != op(e2,e3) & (op(e2,e1) != op(e2,e4) & (op(e2,e2) != op(e2,e3) & (op(e2,e2) != op(e2,e4) & (op(e2,e3) != op(e2,e4) & (op(e3,e0) != op(e3,e1) & (op(e3,e0) != op(e3,e2) & (op(e3,e0) != op(e3,e3) & (op(e3,e0) != op(e3,e4) & (op(e3,e1) != op(e3,e2) & (op(e3,e1) != op(e3,e3) & (op(e3,e1) != op(e3,e4) & (op(e3,e2) != op(e3,e3) & (op(e3,e2) != op(e3,e4) & (op(e3,e3) != op(e3,e4) & (op(e4,e0) != op(e4,e1) & (op(e4,e0) != op(e4,e2) & (op(e4,e0) != op(e4,e3) & (op(e4,e0) != op(e4,e4) & (op(e4,e1) != op(e4,e2) & (op(e4,e1) != op(e4,e3) & (op(e4,e1) != op(e4,e4) & (op(e4,e2) != op(e4,e3) & (op(e4,e2) != op(e4,e4) & op(e4,e3) != op(e4,e4))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 160.72/24.13 fof(ax5, axiom, (e0 != e1 & (e0 != e2 & (e0 != e3 & (e0 != e4 & (e1 != e2 & (e1 != e3 & (e1 != e4 & (e2 != e3 & (e2 != e4 & e3 != e4)))))))))). % 160.72/24.13 fof(ax6, axiom, (e0 = op(op(e2,e2),op(e2,e2)) & (e1 = op(op(e2,op(e2,e2)),op(e2,e2)) & (e3 = op(e2,op(e2,e2)) & e4 = op(e2,e2))))). % 160.72/24.13 fof(co1, conjecture, ~((((op(e0,op(e0,e0)) != e0 & op(e0,op(e0,e0)) = e0) | ((op(e1,op(e1,e0)) != e0 & op(e0,op(e1,e0)) = e1) | ((op(e2,op(e2,e0)) != e0 & op(e0,op(e2,e0)) = e2) | ((op(e3,op(e3,e0)) != e0 & op(e0,op(e3,e0)) = e3) | (op(e4,op(e4,e0)) != e0 & op(e0,op(e4,e0)) = e4))))) & (((op(e0,op(e0,e1)) != e1 & op(e1,op(e0,e1)) = e0) | ((op(e1,op(e1,e1)) != e1 & op(e1,op(e1,e1)) = e1) | ((op(e2,op(e2,e1)) != e1 & op(e1,op(e2,e1)) = e2) | ((op(e3,op(e3,e1)) != e1 & op(e1,op(e3,e1)) = e3) | (op(e4,op(e4,e1)) != e1 & op(e1,op(e4,e1)) = e4))))) & (((op(e0,op(e0,e2)) != e2 & op(e2,op(e0,e2)) = e0) | ((op(e1,op(e1,e2)) != e2 & op(e2,op(e1,e2)) = e1) | ((op(e2,op(e2,e2)) != e2 & op(e2,op(e2,e2)) = e2) | ((op(e3,op(e3,e2)) != e2 & op(e2,op(e3,e2)) = e3) | (op(e4,op(e4,e2)) != e2 & op(e2,op(e4,e2)) = e4))))) & (((op(e0,op(e0,e3)) != e3 & op(e3,op(e0,e3)) = e0) | ((op(e1,op(e1,e3)) != e3 & op(e3,op(e1,e3)) = e1) | ((op(e2,op(e2,e3)) != e3 & op(e3,op(e2,e3)) = e2) | ((op(e3,op(e3,e3)) != e3 & op(e3,op(e3,e3)) = e3) | (op(e4,op(e4,e3)) != e3 & op(e3,op(e4,e3)) = e4))))) & (((op(e0,op(e0,e4)) != e4 & op(e4,op(e0,e4)) = e0) | ((op(e1,op(e1,e4)) != e4 & op(e4,op(e1,e4)) = e1) | ((op(e2,op(e2,e4)) != e4 & op(e4,op(e2,e4)) = e2) | ((op(e3,op(e3,e4)) != e4 & op(e4,op(e3,e4)) = e3) | (op(e4,op(e4,e4)) != e4 & op(e4,op(e4,e4)) = e4))))) & ((op(e0,e0) = e0 & (op(e0,e0) = e0 & op(e0,e0) != e0)) | ((op(e0,e0) = e1 & (op(e1,e1) = e0 & op(e0,e1) != e0)) | ((op(e0,e0) = e2 & (op(e2,e2) = e0 & op(e0,e2) != e0)) | ((op(e0,e0) = e3 & (op(e3,e3) = e0 & op(e0,e3) != e0)) | ((op(e0,e0) = e4 & (op(e4,e4) = e0 & op(e0,e4) != e0)) | ((op(e1,e1) = e0 & (op(e0,e0) = e1 & op(e1,e0) != e1)) | ((op(e1,e1) = e1 & (op(e1,e1) = e1 & op(e1,e1) != e1)) | ((op(e1,e1) = e2 & (op(e2,e2) = e1 & op(e1,e2) != e1)) | ((op(e1,e1) = e3 & (op(e3,e3) = e1 & op(e1,e3) != e1)) | ((op(e1,e1) = e4 & (op(e4,e4) = e1 & op(e1,e4) != e1)) | ((op(e2,e2) = e0 & (op(e0,e0) = e2 & op(e2,e0) != e2)) | ((op(e2,e2) = e1 & (op(e1,e1) = e2 & op(e2,e1) != e2)) | ((op(e2,e2) = e2 & (op(e2,e2) = e2 & op(e2,e2) != e2)) | ((op(e2,e2) = e3 & (op(e3,e3) = e2 & op(e2,e3) != e2)) | ((op(e2,e2) = e4 & (op(e4,e4) = e2 & op(e2,e4) != e2)) | ((op(e3,e3) = e0 & (op(e0,e0) = e3 & op(e3,e0) != e3)) | ((op(e3,e3) = e1 & (op(e1,e1) = e3 & op(e3,e1) != e3)) | ((op(e3,e3) = e2 & (op(e2,e2) = e3 & op(e3,e2) != e3)) | ((op(e3,e3) = e3 & (op(e3,e3) = e3 & op(e3,e3) != e3)) | ((op(e3,e3) = e4 & (op(e4,e4) = e3 & op(e3,e4) != e3)) | ((op(e4,e4) = e0 & (op(e0,e0) = e4 & op(e4,e0) != e4)) | ((op(e4,e4) = e1 & (op(e1,e1) = e4 & op(e4,e1) != e4)) | ((op(e4,e4) = e2 & (op(e2,e2) = e4 & op(e4,e2) != e4)) | ((op(e4,e4) = e3 & (op(e3,e3) = e4 & op(e4,e3) != e4)) | (op(e4,e4) = e4 & (op(e4,e4) = e4 & op(e4,e4) != e4))))))))))))))))))))))))))))))))). % 160.72/24.13 fof(negated_conjecture, negated_conjecture, ~~((((op(e0,op(e0,e0)) != e0 & op(e0,op(e0,e0)) = e0) | ((op(e1,op(e1,e0)) != e0 & op(e0,op(e1,e0)) = e1) | ((op(e2,op(e2,e0)) != e0 & op(e0,op(e2,e0)) = e2) | ((op(e3,op(e3,e0)) != e0 & op(e0,op(e3,e0)) = e3) | (op(e4,op(e4,e0)) != e0 & op(e0,op(e4,e0)) = e4))))) & (((op(e0,op(e0,e1)) != e1 & op(e1,op(e0,e1)) = e0) | ((op(e1,op(e1,e1)) != e1 & op(e1,op(e1,e1)) = e1) | ((op(e2,op(e2,e1)) != e1 & op(e1,op(e2,e1)) = e2) | ((op(e3,op(e3,e1)) != e1 & op(e1,op(e3,e1)) = e3) | (op(e4,op(e4,e1)) != e1 & op(e1,op(e4,e1)) = e4))))) & (((op(e0,op(e0,e2)) != e2 & op(e2,op(e0,e2)) = e0) | ((op(e1,op(e1,e2)) != e2 & op(e2,op(e1,e2)) = e1) | ((op(e2,op(e2,e2)) != e2 & op(e2,op(e2,e2)) = e2) | ((op(e3,op(e3,e2)) != e2 & op(e2,op(e3,e2)) = e3) | (op(e4,op(e4,e2)) != e2 & op(e2,op(e4,e2)) = e4))))) & (((op(e0,op(e0,e3)) != e3 & op(e3,op(e0,e3)) = e0) | ((op(e1,op(e1,e3)) != e3 & op(e3,op(e1,e3)) = e1) | ((op(e2,op(e2,e3)) != e3 & op(e3,op(e2,e3)) = e2) | ((op(e3,op(e3,e3)) != e3 & op(e3,op(e3,e3)) = e3) | (op(e4,op(e4,e3)) != e3 & op(e3,op(e4,e3)) = e4))))) & (((op(e0,op(e0,e4)) != e4 & op(e4,op(e0,e4)) = e0) | ((op(e1,op(e1,e4)) != e4 & op(e4,op(e1,e4)) = e1) | ((op(e2,op(e2,e4)) != e4 & op(e4,op(e2,e4)) = e2) | ((op(e3,op(e3,e4)) != e4 & op(e4,op(e3,e4)) = e3) | (op(e4,op(e4,e4)) != e4 & op(e4,op(e4,e4)) = e4))))) & ((op(e0,e0) = e0 & (op(e0,e0) = e0 & op(e0,e0) != e0)) | ((op(e0,e0) = e1 & (op(e1,e1) = e0 & op(e0,e1) != e0)) | ((op(e0,e0) = e2 & (op(e2,e2) = e0 & op(e0,e2) != e0)) | ((op(e0,e0) = e3 & (op(e3,e3) = e0 & op(e0,e3) != e0)) | ((op(e0,e0) = e4 & (op(e4,e4) = e0 & op(e0,e4) != e0)) | ((op(e1,e1) = e0 & (op(e0,e0) = e1 & op(e1,e0) != e1)) | ((op(e1,e1) = e1 & (op(e1,e1) = e1 & op(e1,e1) != e1)) | ((op(e1,e1) = e2 & (op(e2,e2) = e1 & op(e1,e2) != e1)) | ((op(e1,e1) = e3 & (op(e3,e3) = e1 & op(e1,e3) != e1)) | ((op(e1,e1) = e4 & (op(e4,e4) = e1 & op(e1,e4) != e1)) | ((op(e2,e2) = e0 & (op(e0,e0) = e2 & op(e2,e0) != e2)) | ((op(e2,e2) = e1 & (op(e1,e1) = e2 & op(e2,e1) != e2)) | ((op(e2,e2) = e2 & (op(e2,e2) = e2 & op(e2,e2) != e2)) | ((op(e2,e2) = e3 & (op(e3,e3) = e2 & op(e2,e3) != e2)) | ((op(e2,e2) = e4 & (op(e4,e4) = e2 & op(e2,e4) != e2)) | ((op(e3,e3) = e0 & (op(e0,e0) = e3 & op(e3,e0) != e3)) | ((op(e3,e3) = e1 & (op(e1,e1) = e3 & op(e3,e1) != e3)) | ((op(e3,e3) = e2 & (op(e2,e2) = e3 & op(e3,e2) != e3)) | ((op(e3,e3) = e3 & (op(e3,e3) = e3 & op(e3,e3) != e3)) | ((op(e3,e3) = e4 & (op(e4,e4) = e3 & op(e3,e4) != e3)) | ((op(e4,e4) = e0 & (op(e0,e0) = e4 & op(e4,e0) != e4)) | ((op(e4,e4) = e1 & (op(e1,e1) = e4 & op(e4,e1) != e4)) | ((op(e4,e4) = e2 & (op(e2,e2) = e4 & op(e4,e2) != e4)) | ((op(e4,e4) = e3 & (op(e3,e3) = e4 & op(e4,e3) != e4)) | (op(e4,e4) = e4 & (op(e4,e4) = e4 & op(e4,e4) != e4)))))))))))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 160.72/24.13 cnf(c2, plain, op(e0,e4) = e2 | op(e0,e4) = e4 | op(e0,e4) = e3 | op(e0,e4) = e1 | op(e0,e4) = e0, inference(clausification, [status(esa)], [ax1])). % 160.72/24.13 cnf(c5, plain, op(e2,e0) = e3 | op(e2,e0) = e2 | op(e2,e0) = e4 | op(e2,e0) = e1 | op(e2,e0) = e0, inference(clausification, [status(esa)], [ax1])). % 160.72/24.13 cnf(c10, plain, op(e4,e0) = e1 | op(e4,e0) = e2 | op(e4,e0) = e0 | op(e4,e0) = e4 | op(e4,e0) = e3, inference(clausification, [status(esa)], [ax1])). % 160.72/24.13 cnf(c17, plain, op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e4 | op(e3,e0) = e3 | op(e3,e0) = e2, inference(clausification, [status(esa)], [ax1])). % 160.72/24.13 cnf(c23, plain, op(e0,e3) = e2 | op(e0,e3) = e4 | op(e0,e3) = e1 | op(e0,e3) = e0 | op(e0,e3) = e3, inference(clausification, [status(esa)], [ax1])). % 160.72/24.13 cnf(c25, plain, op(unit,e0) = e0, inference(clausification, [status(esa)], [ax2])). % 160.72/24.13 cnf(c26, plain, op(unit,e1) = e1, inference(clausification, [status(esa)], [ax2])). % 160.72/24.13 cnf(c27, plain, op(unit,e2) = e2, inference(clausification, [status(esa)], [ax2])). % 160.72/24.13 cnf(c28, plain, op(unit,e3) = e3, inference(clausification, [status(esa)], [ax2])). % 160.72/24.13 cnf(c29, plain, op(unit,e4) = e4, inference(clausification, [status(esa)], [ax2])). % 160.72/24.13 cnf(c30, plain, unit = e1 | unit = e0 | unit = e4 | unit = e3 | unit = e2, inference(clausification, [status(esa)], [ax2])). % 160.72/24.13 cnf(c31, plain, op(e4,unit) = e4, inference(clausification, [status(esa)], [ax2])). % 160.72/24.13 cnf(c32, plain, op(e3,unit) = e3, inference(clausification, [status(esa)], [ax2])). % 160.72/24.13 cnf(c33, plain, op(e2,unit) = e2, inference(clausification, [status(esa)], [ax2])). % 160.72/24.13 cnf(c34, plain, op(e1,unit) = e1, inference(clausification, [status(esa)], [ax2])). % 160.72/24.13 cnf(c35, plain, op(e0,unit) = e0, inference(clausification, [status(esa)], [ax2])). % 160.72/24.13 cnf(c41, plain, op(e1,e4) = e0 | op(e1,e0) = e0 | op(e1,e2) = e0 | op(e1,e3) = e0 | op(e1,e1) = e0, inference(clausification, [status(esa)], [ax3])). % 160.72/24.13 cnf(c46, plain, op(e2,e0) = e0 | op(e2,e3) = e0 | op(e2,e4) = e0 | op(e2,e1) = e0 | op(e2,e2) = e0, inference(clausification, [status(esa)], [ax3])). % 160.72/24.13 cnf(c47, plain, op(e2,e0) = e1 | op(e2,e1) = e1 | op(e2,e3) = e1 | op(e2,e4) = e1 | op(e2,e2) = e1, inference(clausification, [status(esa)], [ax3])). % 160.72/24.13 cnf(c51, plain, op(e3,e0) = e0 | op(e3,e4) = e0 | op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0, inference(clausification, [status(esa)], [ax3])). % 160.72/24.13 cnf(c82, plain, op(e2,e0) = e3 | op(e0,e0) = e3 | op(e3,e0) = e3 | op(e1,e0) = e3 | op(e4,e0) = e3, inference(clausification, [status(esa)], [ax3])). % 160.72/24.13 cnf(c87, plain, op(e3,e0) != op(e0,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c88, plain, op(e2,e0) != op(e1,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c89, plain, op(e4,e0) != op(e1,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c90, plain, op(e4,e0) != op(e2,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c93, plain, op(e2,e1) != op(e1,e1), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c101, plain, op(e1,e3) != op(e0,e3), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c103, plain, op(e2,e3) != op(e1,e3), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c106, plain, op(e1,e4) != op(e0,e4), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c107, plain, op(e3,e4) != op(e0,e4), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c110, plain, op(e4,e4) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c112, plain, op(e0,e3) != op(e0,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c114, plain, op(e0,e4) != op(e0,e1), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c117, plain, op(e1,e3) != op(e1,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c121, plain, op(e2,e1) != op(e2,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c125, plain, op(e2,e4) != op(e2,e2), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c126, plain, op(e3,e1) != op(e3,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c129, plain, op(e3,e4) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c134, plain, op(e4,e4) != op(e4,e1), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c135, plain, op(e4,e4) != op(e4,e2), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c141, plain, op(e3,e4) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c148, plain, op(e2,e3) != op(e2,e1), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c149, plain, op(e2,e4) != op(e2,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c150, plain, op(e2,e2) != op(e2,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c151, plain, op(e1,e4) != op(e1,e3), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c156, plain, op(e0,e4) != op(e0,e3), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c158, plain, op(e0,e3) != op(e0,e1), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c160, plain, op(e0,e2) != op(e0,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c161, plain, op(e4,e4) != op(e3,e4), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c165, plain, op(e2,e4) != op(e0,e4), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c167, plain, op(e3,e3) != op(e2,e3), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c172, plain, op(e3,e2) != op(e2,e2), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c177, plain, op(e3,e1) != op(e2,e1), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c180, plain, op(e2,e1) != op(e0,e1), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c182, plain, op(e3,e0) != op(e2,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c184, plain, op(e4,e0) != op(e0,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c185, plain, op(e2,e0) != op(e0,e0), inference(clausification, [status(esa)], [ax4])). % 160.72/24.13 cnf(c186, plain, e1 != e0, inference(clausification, [status(esa)], [ax5])). % 160.72/24.13 cnf(c187, plain, e3 != e0, inference(clausification, [status(esa)], [ax5])). % 160.72/24.13 cnf(c188, plain, e2 != e1, inference(clausification, [status(esa)], [ax5])). % 160.72/24.13 cnf(c189, plain, e4 != e1, inference(clausification, [status(esa)], [ax5])). % 160.72/24.13 cnf(c190, plain, e4 != e2, inference(clausification, [status(esa)], [ax5])). % 160.72/24.13 cnf(c191, plain, e4 != e3, inference(clausification, [status(esa)], [ax5])). % 160.72/24.13 cnf(c192, plain, e3 != e2, inference(clausification, [status(esa)], [ax5])). % 160.72/24.13 cnf(c193, plain, e3 != e1, inference(clausification, [status(esa)], [ax5])). % 160.72/24.13 cnf(c194, plain, e4 != e0, inference(clausification, [status(esa)], [ax5])). % 160.72/24.13 cnf(c195, plain, e2 != e0, inference(clausification, [status(esa)], [ax5])). % 160.72/24.13 cnf(c196, plain, op(op(e2,e2),op(e2,e2)) = e0, inference(clausification, [status(esa)], [ax6])). % 160.72/24.13 cnf(c197, plain, op(e2,op(e2,e2)) = e3, inference(clausification, [status(esa)], [ax6])). % 160.72/24.13 cnf(c198, plain, op(e2,e2) = e4, inference(clausification, [status(esa)], [ax6])). % 160.72/24.13 cnf(c199, plain, op(op(e2,op(e2,e2)),op(e2,e2)) = e1, inference(clausification, [status(esa)], [ax6])). % 160.72/24.13 cnf(c200, plain, X0 | op(e3,op(e3,e0)) != e0 | op(e1,op(e1,e0)) != e0, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c201, plain, X0 | op(e3,op(e3,e0)) != e0 | op(e0,op(e1,e0)) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c203, plain, X0 | op(e0,op(e3,e0)) = e3 | op(e0,op(e1,e0)) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c210, plain, X0 | op(e4,op(e3,e4)) = e3 | op(e1,op(e1,e4)) != e4, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c212, plain, X0 | op(e0,e0) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c214, plain, X0 | op(e1,e1) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c217, plain, X0 | op(e3,op(e4,e3)) = e4 | op(e1,op(e1,e3)) != e3, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c226, plain, ~X0 | op(e0,op(e2,e0)) = e2 | op(e0,op(e4,e0)) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c234, plain, ~X0 | op(e4,op(e0,e4)) = e0 | op(e4,op(e2,e4)) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c237, plain, ~X0 | op(e2,e2) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c238, plain, ~X0 | X1 | op(e0,e0) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c243, plain, ~X0 | X1 | op(e3,e3) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c244, plain, ~X0 | X1 | op(e2,e2) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c249, plain, ~X0 | X1 | op(e4,e4) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c250, plain, ~X0 | X1 | op(e3,e3) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c254, plain, ~X0 | X1 | op(e4,e0) != e4, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c255, plain, ~X0 | X1 | op(e0,e0) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c256, plain, ~X0 | X1 | op(e4,e4) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c259, plain, ~X0 | X1 | op(e4,e4) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c262, plain, ~X0 | X1 | op(e4,e4) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c267, plain, ~X0 | X1 | op(e4,e4) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c270, plain, ~X0 | X1 | op(e2,e2) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c271, plain, ~X0 | X1 | op(e3,e3) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c272, plain, ~X0 | X1 | op(e3,e0) != e3, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c274, plain, ~X0 | X1 | op(e2,e2) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c277, plain, ~X0 | X1 | op(e2,e2) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c282, plain, ~X0 | X1 | op(e4,e4) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c285, plain, ~X0 | X1 | op(e2,e2) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c286, plain, ~X0 | X1 | op(e1,e1) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c287, plain, ~X0 | X1 | op(e1,e0) != e1, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c288, plain, ~X0 | X1 | op(e0,e0) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c289, plain, ~X0 | X1 | op(e0,e0) = e3, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c291, plain, ~X0 | X1 | op(e3,e3) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(c295, plain, ~X0 | op(e3,op(e0,e3)) = e0 | op(e3,op(e2,e3)) = e2, inference(clausification, [status(esa)], [negated_conjecture])). % 160.72/24.13 cnf(d0, plain, op(e2,e4) = e3, inference(demodulation, [status(thm)], [c197,c198])). % 160.72/24.13 cnf(d1, plain, op(op(e2,e4),op(e2,e2)) = e1, inference(demodulation, [status(thm)], [c199,c198])). % 160.72/24.13 cnf(d2, plain, op(op(e2,e4),e4) = e1, inference(demodulation, [status(thm)], [d1,c198])). % 160.72/24.13 cnf(d3, plain, op(e3,e4) = e1, inference(demodulation, [status(thm)], [d2,d0])). % 160.72/24.13 cnf(d4, plain, e1 != op(e3,e1), inference(demodulation, [status(thm)], [c129,d3])). % 160.72/24.13 cnf(d5, plain, op(e4,e0) = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c30,c31])). % 160.72/24.13 cnf(d6, plain, e4 = e0 | ~'Ts3', inference(demodulation, [status(thm)], [c237,c198])). % 160.72/24.13 cnf(d7, plain, ~'Ts3', inference(resolution, [status(thm)], [c194,d6])). % 160.72/24.13 cnf(d8, plain, op(e0,e0) = e4 | ~'Ts4', inference(resolution, [status(thm)], [d7,c238])). % 160.72/24.13 cnf(d9, plain, e1 != op(e3,e3), inference(demodulation, [status(thm)], [c141,d3])). % 160.72/24.13 cnf(d10, plain, e4 = e0 | 'Ts5' | ~'Ts6', inference(demodulation, [status(thm)], [c244,c198])). % 160.72/24.13 cnf(d11, plain, 'Ts5' | ~'Ts6', inference(resolution, [status(thm)], [c194,d10])). % 160.72/24.13 cnf(d12, plain, op(e4,op(e2,e2)) = e0, inference(demodulation, [status(thm)], [c196,c198])). % 160.72/24.13 cnf(d13, plain, op(e4,e4) = e0, inference(demodulation, [status(thm)], [d12,c198])). % 160.72/24.13 cnf(d14, plain, e0 = e2 | 'Ts6' | ~'Ts7', inference(demodulation, [status(thm)], [c249,d13])). % 160.72/24.13 cnf(d15, plain, e4 != e4 | 'Ts8' | ~'Ts9' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d5,c254])). % 160.72/24.13 cnf(d16, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts8' | ~'Ts9', inference(equality_resolution, [status(thm)], [d15])). % 160.72/24.13 cnf(d17, plain, e0 = e2 | 'Ts9' | ~'Ts10', inference(demodulation, [status(thm)], [c256,d13])). % 160.72/24.13 cnf(d18, plain, e0 = e3 | 'Ts10' | ~'Ts11', inference(demodulation, [status(thm)], [c259,d13])). % 160.72/24.13 cnf(d19, plain, e0 = e1 | 'Ts11' | ~'Ts12', inference(demodulation, [status(thm)], [c262,d13])). % 160.72/24.13 cnf(d20, plain, e0 = e3 | 'Ts12' | ~'Ts13', inference(demodulation, [status(thm)], [c267,d13])). % 160.72/24.13 cnf(d21, plain, e4 = e3 | 'Ts13' | ~'Ts14', inference(demodulation, [status(thm)], [c270,c198])). % 160.72/24.13 cnf(d22, plain, 'Ts13' | ~'Ts14', inference(resolution, [status(thm)], [c191,d21])). % 160.72/24.13 cnf(d23, plain, e4 = e3 | 'Ts15' | ~'Ts16', inference(demodulation, [status(thm)], [c274,c198])). % 160.72/24.13 cnf(d24, plain, 'Ts15' | ~'Ts16', inference(resolution, [status(thm)], [c191,d23])). % 160.72/24.13 cnf(d25, plain, e4 = e1 | 'Ts16' | ~'Ts17', inference(demodulation, [status(thm)], [c277,c198])). % 160.72/24.13 cnf(d26, plain, 'Ts16' | ~'Ts17', inference(resolution, [status(thm)], [c189,d25])). % 160.72/24.13 cnf(d27, plain, e0 = e1 | 'Ts17' | ~'Ts18', inference(demodulation, [status(thm)], [c282,d13])). % 160.72/24.13 cnf(d28, plain, e4 = e1 | 'Ts18' | ~'Ts19', inference(demodulation, [status(thm)], [c285,c198])). % 160.72/24.13 cnf(d29, plain, 'Ts18' | ~'Ts19', inference(resolution, [status(thm)], [c189,d28])). % 160.72/24.13 cnf(d30, plain, op(e0,e0) = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c30,c25])). % 160.72/24.13 cnf(d31, plain, e1 = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [c212,d30])). % 160.72/24.13 cnf(d32, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(resolution, [status(thm)], [c186,d31])). % 160.72/24.13 cnf(d33, plain, op(e3,e1) = e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [d32,c26])). % 160.72/24.13 cnf(d34, plain, e1 != op(e2,e1) | unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [d33,c177])). % 160.72/24.13 cnf(d35, plain, op(e1,e3) = e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [d32,c34])). % 160.72/24.13 cnf(d36, plain, op(e2,e3) != e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [d35,c103])). % 160.72/24.13 cnf(d37, plain, op(e2,e0) != e1 | 'Ts21', inference(superposition, [status(thm)], [c212,c185])). % 160.72/24.13 cnf(d38, plain, e1 != e1 | 'Ts21' | op(e2,e3) = e1 | op(e2,e2) = e1 | op(e2,e4) = e1 | op(e2,e1) = e1, inference(superposition, [status(thm)], [c47,d37])). % 160.72/24.13 cnf(d39, plain, op(e2,e3) = e1 | e4 = e1 | op(e2,e4) = e1 | op(e2,e1) = e1 | e1 != e1 | 'Ts21', inference(demodulation, [status(thm)], [d38,c198])). % 160.72/24.13 cnf(d40, plain, op(e2,e3) = e1 | op(e2,e4) = e1 | op(e2,e1) = e1 | e1 != e1 | 'Ts21', inference(resolution, [status(thm)], [c189,d39])). % 160.72/24.13 cnf(d41, plain, op(e2,e3) = e1 | op(e2,e4) = e1 | op(e2,e1) = e1 | 'Ts21', inference(equality_resolution, [status(thm)], [d40])). % 160.72/24.13 cnf(d42, plain, e1 != e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts21' | op(e2,e4) = e1 | op(e2,e1) = e1 | 'Ts21', inference(superposition, [status(thm)], [d41,d36])). % 160.72/24.13 cnf(d43, plain, op(e2,e4) = e1 | op(e2,e1) = e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(equality_resolution, [status(thm)], [d42])). % 160.72/24.13 cnf(d44, plain, op(e1,e4) = e1 | op(e2,e1) = e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [d43,d2])). % 160.72/24.14 cnf(d45, plain, e1 != e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts21' | op(e1,e4) = e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [d44,d34])). % 160.72/24.14 cnf(d46, plain, op(e1,e4) = e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(equality_resolution, [status(thm)], [d45])). % 160.72/24.14 cnf(d47, plain, e1 != op(e1,e3) | unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [d46,c151])). % 160.72/24.14 cnf(d48, plain, e1 != e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts21' | unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [d35,d47])). % 160.72/24.14 cnf(d49, plain, unit = e2 | unit = e4 | unit = e1 | 'Ts21', inference(equality_resolution, [status(thm)], [d48])). % 160.72/24.14 cnf(d50, plain, op(e2,e2) = e2 | unit = e4 | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [d49,c33])). % 160.72/24.14 cnf(d51, plain, e4 = e2 | unit = e4 | unit = e1 | 'Ts21', inference(demodulation, [status(thm)], [d50,c198])). % 160.72/24.14 cnf(d52, plain, unit = e4 | unit = e1 | 'Ts21', inference(resolution, [status(thm)], [c190,d51])). % 160.72/24.14 cnf(d53, plain, op(e2,e4) = e2 | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [d52,c33])). % 160.72/24.14 cnf(d54, plain, op(e2,e4) = e1 | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [d53,d2])). % 160.72/24.14 cnf(d55, plain, e2 = e1 | unit = e1 | 'Ts21' | unit = e1 | 'Ts21', inference(superposition, [status(thm)], [d53,d54])). % 160.72/24.14 cnf(d56, plain, unit = e1 | 'Ts21', inference(resolution, [status(thm)], [c188,d55])). % 160.72/24.14 cnf(d57, plain, op(e1,e1) = e1 | 'Ts21', inference(superposition, [status(thm)], [d56,c26])). % 160.72/24.14 cnf(d58, plain, e1 = e0 | 'Ts21' | 'Ts21', inference(superposition, [status(thm)], [d57,c214])). % 160.72/24.14 cnf(d59, plain, 'Ts21', inference(resolution, [status(thm)], [c186,d58])). % 160.72/24.14 cnf(d60, plain, op(e3,e3) = e0 | 'Ts20', inference(resolution, [status(thm)], [d59,c291])). % 160.72/24.14 cnf(d61, plain, op(e0,e0) = e3 | 'Ts20', inference(resolution, [status(thm)], [d59,c289])). % 160.72/24.14 cnf(d62, plain, e3 = e0 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts20', inference(superposition, [status(thm)], [d61,d30])). % 160.72/24.14 cnf(d63, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts20', inference(resolution, [status(thm)], [c187,d62])). % 160.72/24.14 cnf(d64, plain, op(e3,e3) = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts20', inference(superposition, [status(thm)], [d63,c28])). % 160.72/24.14 cnf(d65, plain, e3 = e0 | 'Ts20' | unit = e2 | unit = e4 | unit = e1 | 'Ts20', inference(superposition, [status(thm)], [d64,d60])). % 160.72/24.14 cnf(d66, plain, unit = e2 | unit = e4 | unit = e1 | 'Ts20', inference(resolution, [status(thm)], [c187,d65])). % 160.72/24.14 cnf(d67, plain, op(e2,e2) = e2 | unit = e4 | unit = e1 | 'Ts20', inference(superposition, [status(thm)], [d66,c33])). % 160.72/24.14 cnf(d68, plain, e4 = e2 | unit = e4 | unit = e1 | 'Ts20', inference(demodulation, [status(thm)], [d67,c198])). % 160.72/24.14 cnf(d69, plain, unit = e4 | unit = e1 | 'Ts20', inference(resolution, [status(thm)], [c190,d68])). % 160.72/24.14 cnf(d70, plain, op(e2,e4) = e2 | unit = e1 | 'Ts20', inference(superposition, [status(thm)], [d69,c33])). % 160.72/24.14 cnf(d71, plain, op(e2,e4) = e1 | unit = e1 | 'Ts20', inference(superposition, [status(thm)], [d70,d2])). % 160.72/24.14 cnf(d72, plain, e2 = e1 | unit = e1 | 'Ts20' | unit = e1 | 'Ts20', inference(superposition, [status(thm)], [d70,d71])). % 160.72/24.14 cnf(d73, plain, unit = e1 | 'Ts20', inference(resolution, [status(thm)], [c188,d72])). % 160.72/24.14 cnf(d74, plain, op(e0,e1) = e0 | 'Ts20', inference(superposition, [status(thm)], [d73,c35])). % 160.72/24.14 cnf(d75, plain, op(e2,e1) != e0 | 'Ts20', inference(superposition, [status(thm)], [d74,c180])). % 160.72/24.14 cnf(d76, plain, e0 != op(e2,e3) | 'Ts20', inference(superposition, [status(thm)], [d60,c167])). % 160.72/24.14 cnf(d77, plain, op(e1,e0) = e0 | 'Ts20', inference(superposition, [status(thm)], [d73,c25])). % 160.72/24.14 cnf(d78, plain, op(e2,e0) != e0 | 'Ts20', inference(superposition, [status(thm)], [d77,c88])). % 160.72/24.14 cnf(d79, plain, op(e2,e0) = e0 | op(e2,e3) = e0 | e4 = e0 | op(e2,e4) = e0 | op(e2,e1) = e0, inference(demodulation, [status(thm)], [c46,c198])). % 160.72/24.14 cnf(d80, plain, op(e2,e0) = e0 | op(e2,e3) = e0 | e3 = e0 | op(e2,e1) = e0 | e4 = e0, inference(demodulation, [status(thm)], [d79,d0])). % 160.72/24.14 cnf(d81, plain, op(e2,e0) = e0 | op(e2,e3) = e0 | op(e2,e1) = e0 | e4 = e0, inference(resolution, [status(thm)], [c187,d80])). % 160.72/24.14 cnf(d82, plain, op(e2,e0) = e0 | op(e2,e3) = e0 | op(e2,e1) = e0, inference(resolution, [status(thm)], [c194,d81])). % 160.72/24.14 cnf(d83, plain, e0 != e0 | 'Ts20' | op(e2,e3) = e0 | op(e2,e1) = e0, inference(superposition, [status(thm)], [d82,d78])). % 160.72/24.14 cnf(d84, plain, op(e2,e3) = e0 | op(e2,e1) = e0 | 'Ts20', inference(equality_resolution, [status(thm)], [d83])). % 160.72/24.14 cnf(d85, plain, e0 != e0 | 'Ts20' | op(e2,e1) = e0 | 'Ts20', inference(superposition, [status(thm)], [d84,d76])). % 160.72/24.14 cnf(d86, plain, op(e2,e1) = e0 | 'Ts20', inference(equality_resolution, [status(thm)], [d85])). % 160.72/24.14 cnf(d87, plain, e0 != e0 | 'Ts20' | 'Ts20', inference(superposition, [status(thm)], [d86,d75])). % 160.72/24.14 cnf(d88, plain, 'Ts20', inference(equality_resolution, [status(thm)], [d87])). % 160.72/24.14 cnf(d89, plain, op(e1,e1) = e0 | 'Ts19', inference(resolution, [status(thm)], [d88,c286])). % 160.72/24.14 cnf(d90, plain, op(e1,e0) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c30,c34])). % 160.72/24.14 cnf(d91, plain, e1 != e1 | 'Ts19' | ~'Ts20' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d90,c287])). % 160.72/24.14 cnf(d92, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts19' | ~'Ts20', inference(equality_resolution, [status(thm)], [d91])). % 160.72/24.14 cnf(d93, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts19', inference(resolution, [status(thm)], [d88,d92])). % 160.72/24.14 cnf(d94, plain, op(e3,e1) = e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts19', inference(superposition, [status(thm)], [d93,c26])). % 160.72/24.14 cnf(d95, plain, e1 != op(e2,e1) | unit = e2 | unit = e4 | unit = e1 | 'Ts19', inference(superposition, [status(thm)], [d94,c177])). % 160.72/24.14 cnf(d96, plain, op(e0,e0) = e1 | 'Ts19', inference(resolution, [status(thm)], [d88,c288])). % 160.72/24.14 cnf(d97, plain, op(e2,e0) != e1 | 'Ts19', inference(superposition, [status(thm)], [d96,c185])). % 160.72/24.14 cnf(d98, plain, op(e2,e0) = e1 | op(e2,e3) = e1 | e4 = e1 | op(e2,e4) = e1 | op(e2,e1) = e1, inference(demodulation, [status(thm)], [c47,c198])). % 160.72/24.14 cnf(d99, plain, op(e2,e0) = e1 | op(e2,e3) = e1 | e3 = e1 | op(e2,e1) = e1 | e4 = e1, inference(demodulation, [status(thm)], [d98,d0])). % 160.72/24.14 cnf(d100, plain, op(e2,e0) = e1 | op(e2,e3) = e1 | e3 = e1 | op(e2,e1) = e1, inference(resolution, [status(thm)], [c189,d99])). % 160.72/24.14 cnf(d101, plain, op(e2,e0) = e1 | op(e2,e3) = e1 | op(e2,e1) = e1, inference(resolution, [status(thm)], [c193,d100])). % 160.72/24.14 cnf(d102, plain, e1 != e1 | 'Ts19' | op(e2,e3) = e1 | op(e2,e1) = e1, inference(superposition, [status(thm)], [d101,d97])). % 160.72/24.14 cnf(d103, plain, op(e2,e3) = e1 | op(e2,e1) = e1 | 'Ts19', inference(equality_resolution, [status(thm)], [d102])). % 160.72/24.14 cnf(d104, plain, op(e2,e3) = e2 | unit = e2 | unit = e4 | unit = e1 | 'Ts19', inference(superposition, [status(thm)], [d93,c33])). % 160.72/24.14 cnf(d105, plain, e2 = e1 | op(e2,e1) = e1 | 'Ts19' | unit = e2 | unit = e4 | unit = e1 | 'Ts19', inference(superposition, [status(thm)], [d104,d103])). % 160.72/24.14 cnf(d106, plain, op(e2,e1) = e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts19', inference(resolution, [status(thm)], [c188,d105])). % 160.72/24.14 cnf(d107, plain, e1 != e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts19' | unit = e2 | unit = e4 | unit = e1 | 'Ts19', inference(superposition, [status(thm)], [d106,d95])). % 160.72/24.14 cnf(d108, plain, unit = e2 | unit = e4 | unit = e1 | 'Ts19', inference(equality_resolution, [status(thm)], [d107])). % 160.72/24.14 cnf(d109, plain, op(e2,e2) = e2 | unit = e4 | unit = e1 | 'Ts19', inference(superposition, [status(thm)], [d108,c33])). % 160.72/24.14 cnf(d110, plain, e4 = e2 | unit = e4 | unit = e1 | 'Ts19', inference(demodulation, [status(thm)], [d109,c198])). % 160.72/24.14 cnf(d111, plain, unit = e4 | unit = e1 | 'Ts19', inference(resolution, [status(thm)], [c190,d110])). % 160.72/24.14 cnf(d112, plain, op(e2,e4) = e2 | unit = e1 | 'Ts19', inference(superposition, [status(thm)], [d111,c33])). % 160.72/24.14 cnf(d113, plain, e3 = e2 | unit = e1 | 'Ts19', inference(demodulation, [status(thm)], [d112,d0])). % 160.72/24.14 cnf(d114, plain, unit = e1 | 'Ts19', inference(resolution, [status(thm)], [c192,d113])). % 160.72/24.14 cnf(d115, plain, op(e1,e1) = e1 | 'Ts19', inference(superposition, [status(thm)], [d114,c26])). % 160.72/24.14 cnf(d116, plain, e1 = e0 | 'Ts19' | 'Ts19', inference(superposition, [status(thm)], [d115,d89])). % 160.72/24.14 cnf(d117, plain, 'Ts19', inference(resolution, [status(thm)], [c186,d116])). % 160.72/24.14 cnf(d118, plain, 'Ts18', inference(resolution, [status(thm)], [d117,d29])). % 160.72/24.14 cnf(d119, plain, e0 = e1 | 'Ts17', inference(resolution, [status(thm)], [d118,d27])). % 160.72/24.14 cnf(d120, plain, e0 != e0 | 'Ts17', inference(superposition, [status(thm)], [d119,c186])). % 160.72/24.14 cnf(d121, plain, 'Ts17', inference(equality_resolution, [status(thm)], [d120])). % 160.72/24.14 cnf(d122, plain, 'Ts16', inference(resolution, [status(thm)], [d121,d26])). % 160.72/24.14 cnf(d123, plain, 'Ts15', inference(resolution, [status(thm)], [d122,d24])). % 160.72/24.14 cnf(d124, plain, op(e3,e3) = e0 | 'Ts14', inference(resolution, [status(thm)], [d123,c271])). % 160.72/24.14 cnf(d125, plain, op(e3,e0) = e3 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c30,c32])). % 160.72/24.14 cnf(d126, plain, e3 != e3 | 'Ts14' | ~'Ts15' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d125,c272])). % 160.72/24.14 cnf(d127, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts14' | ~'Ts15', inference(equality_resolution, [status(thm)], [d126])). % 160.72/24.14 cnf(d128, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts14', inference(resolution, [status(thm)], [d123,d127])). % 160.72/24.14 cnf(d129, plain, op(e3,e3) = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts14', inference(superposition, [status(thm)], [d128,c28])). % 160.72/24.14 cnf(d130, plain, e3 = e0 | 'Ts14' | unit = e2 | unit = e4 | unit = e1 | 'Ts14', inference(superposition, [status(thm)], [d129,d124])). % 160.72/24.14 cnf(d131, plain, unit = e2 | unit = e4 | unit = e1 | 'Ts14', inference(resolution, [status(thm)], [c187,d130])). % 160.72/24.14 cnf(d132, plain, op(e2,e2) = e2 | unit = e4 | unit = e1 | 'Ts14', inference(superposition, [status(thm)], [d131,c33])). % 160.72/24.14 cnf(d133, plain, e4 = e2 | unit = e4 | unit = e1 | 'Ts14', inference(demodulation, [status(thm)], [d132,c198])). % 160.72/24.14 cnf(d134, plain, unit = e4 | unit = e1 | 'Ts14', inference(resolution, [status(thm)], [c190,d133])). % 160.72/24.14 cnf(d135, plain, op(e2,e4) = e2 | unit = e1 | 'Ts14', inference(superposition, [status(thm)], [d134,c33])). % 160.72/24.14 cnf(d136, plain, e3 = e2 | unit = e1 | 'Ts14', inference(demodulation, [status(thm)], [d135,d0])). % 160.72/24.14 cnf(d137, plain, unit = e1 | 'Ts14', inference(resolution, [status(thm)], [c192,d136])). % 160.72/24.14 cnf(d138, plain, op(e0,e1) = e0 | 'Ts14', inference(superposition, [status(thm)], [d137,c35])). % 160.72/24.14 cnf(d139, plain, op(e2,e1) != e0 | 'Ts14', inference(superposition, [status(thm)], [d138,c180])). % 160.72/24.14 cnf(d140, plain, e0 != op(e2,e3) | 'Ts14', inference(superposition, [status(thm)], [d124,c167])). % 160.72/24.14 cnf(d141, plain, op(e1,e0) = e0 | 'Ts14', inference(superposition, [status(thm)], [d137,c25])). % 160.72/24.14 cnf(d142, plain, op(e2,e0) != e0 | 'Ts14', inference(superposition, [status(thm)], [d141,c88])). % 160.72/24.14 cnf(d143, plain, e0 != e0 | 'Ts14' | op(e2,e3) = e0 | op(e2,e1) = e0, inference(superposition, [status(thm)], [d82,d142])). % 160.72/24.14 cnf(d144, plain, op(e2,e3) = e0 | op(e2,e1) = e0 | 'Ts14', inference(equality_resolution, [status(thm)], [d143])). % 160.72/24.14 cnf(d145, plain, e0 != e0 | 'Ts14' | op(e2,e1) = e0 | 'Ts14', inference(superposition, [status(thm)], [d144,d140])). % 160.72/24.14 cnf(d146, plain, op(e2,e1) = e0 | 'Ts14', inference(equality_resolution, [status(thm)], [d145])). % 160.72/24.14 cnf(d147, plain, e0 != e0 | 'Ts14' | 'Ts14', inference(superposition, [status(thm)], [d146,d139])). % 160.72/24.14 cnf(d148, plain, 'Ts14', inference(equality_resolution, [status(thm)], [d147])). % 160.72/24.14 cnf(d149, plain, 'Ts13', inference(resolution, [status(thm)], [d148,d22])). % 160.72/24.14 cnf(d150, plain, e0 = e3 | 'Ts12', inference(resolution, [status(thm)], [d149,d20])). % 160.72/24.14 cnf(d151, plain, e0 != e0 | 'Ts12', inference(superposition, [status(thm)], [d150,c187])). % 160.72/24.14 cnf(d152, plain, 'Ts12', inference(equality_resolution, [status(thm)], [d151])). % 160.72/24.14 cnf(d153, plain, e0 = e1 | 'Ts11', inference(resolution, [status(thm)], [d152,d19])). % 160.72/24.14 cnf(d154, plain, e0 != e0 | 'Ts11', inference(superposition, [status(thm)], [d153,c186])). % 160.72/24.14 cnf(d155, plain, 'Ts11', inference(equality_resolution, [status(thm)], [d154])). % 160.72/24.14 cnf(d156, plain, e0 = e3 | 'Ts10', inference(resolution, [status(thm)], [d155,d18])). % 160.72/24.14 cnf(d157, plain, e0 != e0 | 'Ts10', inference(superposition, [status(thm)], [d156,c187])). % 160.72/24.14 cnf(d158, plain, 'Ts10', inference(equality_resolution, [status(thm)], [d157])). % 160.72/24.14 cnf(d159, plain, e0 = e2 | 'Ts9', inference(resolution, [status(thm)], [d158,d17])). % 160.72/24.14 cnf(d160, plain, e2 != e2 | 'Ts9', inference(superposition, [status(thm)], [d159,c195])). % 160.72/24.14 cnf(d161, plain, 'Ts9', inference(equality_resolution, [status(thm)], [d160])). % 160.72/24.14 cnf(d162, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts8', inference(resolution, [status(thm)], [d161,d16])). % 160.72/24.14 cnf(d163, plain, op(e3,e1) = e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts8', inference(superposition, [status(thm)], [d162,c26])). % 160.72/24.14 cnf(d164, plain, op(e3,e4) != e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts8', inference(superposition, [status(thm)], [d163,c129])). % 160.72/24.14 cnf(d165, plain, unit = e2 | unit = e4 | unit = e1 | 'Ts8', inference(resolution, [status(thm)], [d3,d164])). % 160.72/24.14 cnf(d166, plain, op(e2,e2) = e2 | unit = e4 | unit = e1 | 'Ts8', inference(superposition, [status(thm)], [d165,c33])). % 160.72/24.14 cnf(d167, plain, e4 = e2 | unit = e4 | unit = e1 | 'Ts8', inference(demodulation, [status(thm)], [d166,c198])). % 160.72/24.14 cnf(d168, plain, unit = e4 | unit = e1 | 'Ts8', inference(resolution, [status(thm)], [c190,d167])). % 160.72/24.14 cnf(d169, plain, op(e2,e4) = e2 | unit = e1 | 'Ts8', inference(superposition, [status(thm)], [d168,c33])). % 160.72/24.14 cnf(d170, plain, e3 = e2 | unit = e1 | 'Ts8', inference(demodulation, [status(thm)], [d169,d0])). % 160.72/24.14 cnf(d171, plain, unit = e1 | 'Ts8', inference(resolution, [status(thm)], [c192,d170])). % 160.72/24.14 cnf(d172, plain, op(e1,e3) = e3 | 'Ts8', inference(superposition, [status(thm)], [d171,c28])). % 160.72/24.14 cnf(d173, plain, e3 != op(e1,e0) | 'Ts8', inference(superposition, [status(thm)], [d172,c117])). % 160.72/24.14 cnf(d174, plain, op(e0,e1) = e0 | 'Ts8', inference(superposition, [status(thm)], [d171,c35])). % 160.72/24.14 cnf(d175, plain, op(e2,e1) != e0 | 'Ts8', inference(superposition, [status(thm)], [d174,c180])). % 160.72/24.14 cnf(d176, plain, op(e3,e1) = e3 | 'Ts8', inference(superposition, [status(thm)], [d171,c32])). % 160.72/24.14 cnf(d177, plain, e1 != op(e0,e4), inference(demodulation, [status(thm)], [c107,d3])). % 160.72/24.14 cnf(d178, plain, op(e1,e4) = e4 | 'Ts8', inference(superposition, [status(thm)], [d171,c29])). % 160.72/24.14 cnf(d179, plain, e4 != op(e0,e4) | 'Ts8', inference(superposition, [status(thm)], [d178,c106])). % 160.72/24.14 cnf(d180, plain, e0 != op(e4,e1), inference(demodulation, [status(thm)], [c134,d13])). % 160.72/24.14 cnf(d181, plain, e0 != op(e4,e2), inference(demodulation, [status(thm)], [c135,d13])). % 160.72/24.14 cnf(d182, plain, op(e1,e3) != e3 | op(e3,op(e4,e3)) = e4 | 'Ts22' | 'Ts8', inference(superposition, [status(thm)], [d172,c217])). % 160.72/24.14 cnf(d183, plain, e3 != e3 | op(e3,op(e4,e3)) = e4 | 'Ts22' | 'Ts8' | 'Ts8', inference(superposition, [status(thm)], [d172,d182])). % 160.72/24.14 cnf(d184, plain, op(e3,op(e4,e3)) = e4 | 'Ts22' | 'Ts8', inference(equality_resolution, [status(thm)], [d183])). % 160.72/24.14 cnf(d185, plain, op(e4,op(e0,e4)) = e0 | op(e4,e3) = e2 | ~'Ts2', inference(demodulation, [status(thm)], [c234,d0])). % 160.72/24.14 cnf(d186, plain, op(e4,e1) = e4 | 'Ts8', inference(superposition, [status(thm)], [d171,c31])). % 160.72/24.14 cnf(d187, plain, op(e4,e1) = e3 | op(e1,op(e1,e4)) != e4 | 'Ts2', inference(demodulation, [status(thm)], [c210,d3])). % 160.72/24.14 cnf(d188, plain, op(e1,e4) != e4 | op(e4,e1) = e3 | 'Ts2' | 'Ts8', inference(superposition, [status(thm)], [d178,d187])). % 160.72/24.14 cnf(d189, plain, e4 != e4 | op(e4,e1) = e3 | 'Ts2' | 'Ts8' | 'Ts8', inference(superposition, [status(thm)], [d178,d188])). % 160.72/24.14 cnf(d190, plain, op(e4,e1) = e3 | 'Ts2' | 'Ts8', inference(equality_resolution, [status(thm)], [d189])). % 160.72/24.14 cnf(d191, plain, e3 = e4 | 'Ts8' | 'Ts2' | 'Ts8', inference(superposition, [status(thm)], [d190,d186])). % 160.72/24.14 cnf(d192, plain, op(e2,e4) != e4, inference(demodulation, [status(thm)], [c125,c198])). % 160.72/24.14 cnf(d193, plain, e3 != e4, inference(demodulation, [status(thm)], [d192,d0])). % 160.72/24.14 cnf(d194, plain, 'Ts2' | 'Ts8', inference(resolution, [status(thm)], [d193,d191])). % 160.72/24.14 cnf(d195, plain, 'Ts8' | op(e4,op(e0,e4)) = e0 | op(e4,e3) = e2, inference(resolution, [status(thm)], [d194,d185])). % 160.72/24.14 cnf(d196, plain, e3 != op(e0,e4), inference(demodulation, [status(thm)], [c165,d0])). % 160.72/24.14 cnf(d197, plain, op(e0,e4) != e0 | 'Ts8', inference(superposition, [status(thm)], [d174,c114])). % 160.72/24.14 cnf(d198, plain, e0 != e0 | 'Ts8' | op(e0,e4) = e3 | op(e0,e4) = e2 | op(e0,e4) = e4 | op(e0,e4) = e1, inference(superposition, [status(thm)], [c2,d197])). % 160.72/24.14 cnf(d199, plain, op(e0,e4) = e3 | op(e0,e4) = e2 | op(e0,e4) = e4 | op(e0,e4) = e1 | 'Ts8', inference(equality_resolution, [status(thm)], [d198])). % 160.72/24.14 cnf(d200, plain, e3 != e3 | op(e0,e4) = e2 | op(e0,e4) = e4 | op(e0,e4) = e1 | 'Ts8', inference(superposition, [status(thm)], [d199,d196])). % 160.72/24.14 cnf(d201, plain, op(e0,e4) = e2 | op(e0,e4) = e4 | op(e0,e4) = e1 | 'Ts8', inference(equality_resolution, [status(thm)], [d200])). % 160.72/24.14 cnf(d202, plain, op(e4,e2) = e0 | op(e4,e3) = e2 | 'Ts8' | op(e0,e4) = e4 | op(e0,e4) = e1 | 'Ts8', inference(superposition, [status(thm)], [d201,d195])). % 160.72/24.14 cnf(d203, plain, e4 != e4 | 'Ts8' | op(e0,e4) = e1 | op(e4,e3) = e2 | op(e4,e2) = e0 | 'Ts8', inference(superposition, [status(thm)], [d202,d179])). % 160.72/24.14 cnf(d204, plain, op(e0,e4) = e1 | op(e4,e3) = e2 | op(e4,e2) = e0 | 'Ts8', inference(equality_resolution, [status(thm)], [d203])). % 160.72/24.14 cnf(d205, plain, op(e4,e1) = e0 | op(e4,e3) = e2 | 'Ts8' | op(e4,e3) = e2 | op(e4,e2) = e0 | 'Ts8', inference(superposition, [status(thm)], [d204,d195])). % 160.72/24.14 cnf(d206, plain, op(e3,e2) = e4 | 'Ts22' | 'Ts8' | op(e4,e2) = e0 | op(e4,e1) = e0 | 'Ts8', inference(superposition, [status(thm)], [d205,d184])). % 160.72/24.14 cnf(d207, plain, op(e3,e2) != e4, inference(demodulation, [status(thm)], [c172,c198])). % 160.72/24.14 cnf(d208, plain, op(e4,e2) = e0 | op(e4,e1) = e0 | 'Ts22' | 'Ts8', inference(resolution, [status(thm)], [d207,d206])). % 160.72/24.14 cnf(d209, plain, e0 != e0 | op(e4,e1) = e0 | 'Ts22' | 'Ts8', inference(superposition, [status(thm)], [d208,d181])). % 160.72/24.14 cnf(d210, plain, op(e4,e1) = e0 | 'Ts22' | 'Ts8', inference(equality_resolution, [status(thm)], [d209])). % 160.72/24.14 cnf(d211, plain, e0 != e0 | 'Ts22' | 'Ts8', inference(superposition, [status(thm)], [d210,d180])). % 160.72/24.14 cnf(d212, plain, 'Ts22' | 'Ts8', inference(equality_resolution, [status(thm)], [d211])). % 160.72/24.14 cnf(d213, plain, 'Ts8' | op(e3,op(e0,e3)) = e0 | op(e3,op(e2,e3)) = e2, inference(resolution, [status(thm)], [d212,c295])). % 160.72/24.14 cnf(d214, plain, e2 != op(e0,e3) | op(e0,e4) = e4 | op(e0,e4) = e1 | 'Ts8', inference(superposition, [status(thm)], [d201,c156])). % 160.72/24.14 cnf(d215, plain, e3 != op(e0,e3) | 'Ts8', inference(superposition, [status(thm)], [d172,c101])). % 160.72/24.14 cnf(d216, plain, op(e0,e3) != e0 | 'Ts8', inference(superposition, [status(thm)], [d174,c158])). % 160.72/24.14 cnf(d217, plain, e0 != e0 | 'Ts8' | op(e0,e3) = e3 | op(e0,e3) = e2 | op(e0,e3) = e4 | op(e0,e3) = e1, inference(superposition, [status(thm)], [c23,d216])). % 160.72/24.14 cnf(d218, plain, op(e0,e3) = e3 | op(e0,e3) = e2 | op(e0,e3) = e4 | op(e0,e3) = e1 | 'Ts8', inference(equality_resolution, [status(thm)], [d217])). % 160.72/24.14 cnf(d219, plain, e3 != e3 | 'Ts8' | op(e0,e3) = e2 | op(e0,e3) = e4 | op(e0,e3) = e1 | 'Ts8', inference(superposition, [status(thm)], [d218,d215])). % 160.72/24.14 cnf(d220, plain, op(e0,e3) = e2 | op(e0,e3) = e4 | op(e0,e3) = e1 | 'Ts8', inference(equality_resolution, [status(thm)], [d219])). % 160.72/24.14 cnf(d221, plain, e2 != e2 | op(e0,e4) = e4 | op(e0,e4) = e1 | 'Ts8' | op(e0,e3) = e4 | op(e0,e3) = e1 | 'Ts8', inference(superposition, [status(thm)], [d220,d214])). % 160.72/24.14 cnf(d222, plain, op(e0,e3) = e4 | op(e0,e3) = e1 | op(e0,e4) = e4 | op(e0,e4) = e1 | 'Ts8', inference(equality_resolution, [status(thm)], [d221])). % 160.72/24.14 cnf(d223, plain, e4 != op(e0,e0) | op(e0,e3) = e1 | op(e0,e4) = e4 | op(e0,e4) = e1 | 'Ts8', inference(superposition, [status(thm)], [d222,c112])). % 160.72/24.14 cnf(d224, plain, op(e0,e0) = e4 | 'Ts8', inference(resolution, [status(thm)], [d161,c255])). % 160.72/24.14 cnf(d225, plain, e4 != e4 | op(e0,e3) = e1 | op(e0,e4) = e4 | op(e0,e4) = e1 | 'Ts8' | 'Ts8', inference(superposition, [status(thm)], [d224,d223])). % 160.72/24.14 cnf(d226, plain, op(e0,e3) = e1 | op(e0,e4) = e4 | op(e0,e4) = e1 | 'Ts8', inference(equality_resolution, [status(thm)], [d225])). % 160.72/24.14 cnf(d227, plain, op(e3,e1) = e0 | op(e3,op(e2,e3)) = e2 | 'Ts8' | op(e0,e4) = e4 | op(e0,e4) = e1 | 'Ts8', inference(superposition, [status(thm)], [d226,d213])). % 160.72/24.14 cnf(d228, plain, e4 != e4 | 'Ts8' | op(e0,e4) = e1 | op(e3,op(e2,e3)) = e2 | op(e3,e1) = e0 | 'Ts8', inference(superposition, [status(thm)], [d227,d179])). % 160.72/24.14 cnf(d229, plain, op(e0,e4) = e1 | op(e3,op(e2,e3)) = e2 | op(e3,e1) = e0 | 'Ts8', inference(equality_resolution, [status(thm)], [d228])). % 160.72/24.14 cnf(d230, plain, e1 != e1 | op(e3,op(e2,e3)) = e2 | op(e3,e1) = e0 | 'Ts8', inference(superposition, [status(thm)], [d229,d177])). % 160.72/24.14 cnf(d231, plain, op(e3,op(e2,e3)) = e2 | op(e3,e1) = e0 | 'Ts8', inference(equality_resolution, [status(thm)], [d230])). % 160.72/24.14 cnf(d232, plain, op(e1,e0) = e0 | 'Ts8', inference(superposition, [status(thm)], [d171,c25])). % 160.72/24.14 cnf(d233, plain, op(e2,e0) != e0 | 'Ts8', inference(superposition, [status(thm)], [d232,c88])). % 160.72/24.14 cnf(d234, plain, e0 != e0 | 'Ts8' | op(e2,e3) = e0 | op(e2,e1) = e0, inference(superposition, [status(thm)], [d82,d233])). % 160.72/24.14 cnf(d235, plain, op(e2,e3) = e0 | op(e2,e1) = e0 | 'Ts8', inference(equality_resolution, [status(thm)], [d234])). % 160.72/24.14 cnf(d236, plain, op(e3,e0) = e2 | op(e3,e1) = e0 | 'Ts8' | op(e2,e1) = e0 | 'Ts8', inference(superposition, [status(thm)], [d235,d231])). % 160.72/24.14 cnf(d237, plain, op(e3,e2) != e0 | op(e1,op(e1,e0)) != e0 | 'Ts0' | op(e3,e1) = e0 | op(e2,e1) = e0 | 'Ts8', inference(superposition, [status(thm)], [d236,c200])). % 160.72/24.14 cnf(d238, plain, op(e3,e0) != e0 | op(e0,op(e1,e0)) = e1 | 'Ts0' | op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e4) = e0 | op(e3,e1) = e0, inference(superposition, [status(thm)], [c51,c201])). % 160.72/24.14 cnf(d239, plain, e0 != e0 | op(e0,op(e1,e0)) = e1 | op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e4) = e0 | op(e3,e1) = e0 | 'Ts0' | op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e4) = e0 | op(e3,e1) = e0, inference(superposition, [status(thm)], [c51,d238])). % 160.72/24.14 cnf(d240, plain, op(e0,op(e1,e0)) = e1 | op(e3,e3) = e0 | op(e3,e2) = e0 | e1 = e0 | op(e3,e1) = e0 | e0 != e0 | 'Ts0', inference(demodulation, [status(thm)], [d239,d3])). % 160.72/24.14 cnf(d241, plain, op(e0,op(e1,e0)) = e1 | op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0 | e0 != e0 | 'Ts0', inference(resolution, [status(thm)], [c186,d240])). % 160.72/24.14 cnf(d242, plain, op(e0,op(e1,e0)) = e1 | op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0 | 'Ts0', inference(equality_resolution, [status(thm)], [d241])). % 160.72/24.14 cnf(d243, plain, op(e0,e0) = e1 | op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0 | 'Ts0' | 'Ts8', inference(superposition, [status(thm)], [d232,d242])). % 160.72/24.14 cnf(d244, plain, e4 = e1 | op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0 | 'Ts0' | 'Ts8' | 'Ts8', inference(superposition, [status(thm)], [d224,d243])). % 160.72/24.14 cnf(d245, plain, op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0 | 'Ts0' | 'Ts8', inference(resolution, [status(thm)], [c189,d244])). % 160.72/24.14 cnf(d246, plain, e0 != op(e2,e3) | op(e3,e2) = e0 | op(e3,e1) = e0 | 'Ts0' | 'Ts8', inference(superposition, [status(thm)], [d245,c167])). % 160.72/24.14 cnf(d247, plain, e0 != e0 | op(e3,e2) = e0 | op(e3,e1) = e0 | 'Ts0' | 'Ts8' | op(e2,e1) = e0 | 'Ts8', inference(superposition, [status(thm)], [d235,d246])). % 160.72/24.14 cnf(d248, plain, op(e3,e2) = e0 | op(e3,e1) = e0 | op(e2,e1) = e0 | 'Ts0' | 'Ts8', inference(equality_resolution, [status(thm)], [d247])). % 160.72/24.14 cnf(d249, plain, e0 != e0 | op(e3,e1) = e0 | op(e2,e1) = e0 | op(e1,op(e1,e0)) != e0 | 'Ts0' | 'Ts8' | op(e3,e1) = e0 | op(e2,e1) = e0 | 'Ts0' | 'Ts8', inference(superposition, [status(thm)], [d248,d237])). % 160.72/24.14 cnf(d250, plain, op(e1,e0) != e0 | op(e3,e1) = e0 | op(e2,e1) = e0 | e0 != e0 | 'Ts0' | 'Ts8' | 'Ts8', inference(superposition, [status(thm)], [d232,d249])). % 160.72/24.14 cnf(d251, plain, e0 != e0 | op(e3,e1) = e0 | op(e2,e1) = e0 | e0 != e0 | 'Ts0' | 'Ts8' | 'Ts8', inference(superposition, [status(thm)], [d232,d250])). % 160.72/24.14 cnf(d252, plain, op(e3,e1) = e0 | op(e2,e1) = e0 | 'Ts0' | 'Ts8', inference(equality_resolution, [status(thm)], [d251])). % 160.72/24.14 cnf(d253, plain, e0 = e3 | 'Ts8' | op(e2,e1) = e0 | 'Ts0' | 'Ts8', inference(superposition, [status(thm)], [d252,d176])). % 160.72/24.14 cnf(d254, plain, e0 != op(e2,e4), inference(demodulation, [status(thm)], [c110,d13])). % 160.72/24.14 cnf(d255, plain, e0 != e3, inference(demodulation, [status(thm)], [d254,d0])). % 160.72/24.14 cnf(d256, plain, op(e2,e1) = e0 | 'Ts0' | 'Ts8', inference(resolution, [status(thm)], [d255,d253])). % 160.72/24.14 cnf(d257, plain, e0 != e0 | 'Ts8' | 'Ts0' | 'Ts8', inference(superposition, [status(thm)], [d256,d175])). % 160.72/24.14 cnf(d258, plain, 'Ts0' | 'Ts8', inference(equality_resolution, [status(thm)], [d257])). % 160.72/24.14 cnf(d259, plain, 'Ts8' | op(e0,op(e2,e0)) = e2 | op(e0,op(e4,e0)) = e4, inference(resolution, [status(thm)], [d258,c226])). % 160.72/24.14 cnf(d260, plain, e4 != op(e2,e0), inference(demodulation, [status(thm)], [c150,c198])). % 160.72/24.14 cnf(d261, plain, op(e2,e1) = e2 | 'Ts8', inference(superposition, [status(thm)], [d171,c33])). % 160.72/24.14 cnf(d262, plain, e2 != op(e2,e0) | 'Ts8', inference(superposition, [status(thm)], [d261,c121])). % 160.72/24.14 cnf(d263, plain, e3 != op(e2,e0), inference(demodulation, [status(thm)], [c149,d0])). % 160.72/24.14 cnf(d264, plain, e0 != e0 | 'Ts8' | op(e2,e0) = e3 | op(e2,e0) = e2 | op(e2,e0) = e4 | op(e2,e0) = e1, inference(superposition, [status(thm)], [c5,d233])). % 160.72/24.14 cnf(d265, plain, op(e2,e0) = e3 | op(e2,e0) = e2 | op(e2,e0) = e4 | op(e2,e0) = e1 | 'Ts8', inference(equality_resolution, [status(thm)], [d264])). % 160.72/24.14 cnf(d266, plain, e3 != e3 | op(e2,e0) = e2 | op(e2,e0) = e4 | op(e2,e0) = e1 | 'Ts8', inference(superposition, [status(thm)], [d265,d263])). % 160.72/24.14 cnf(d267, plain, op(e2,e0) = e2 | op(e2,e0) = e4 | op(e2,e0) = e1 | 'Ts8', inference(equality_resolution, [status(thm)], [d266])). % 160.72/24.14 cnf(d268, plain, e2 != e2 | 'Ts8' | op(e2,e0) = e4 | op(e2,e0) = e1 | 'Ts8', inference(superposition, [status(thm)], [d267,d262])). % 160.72/24.14 cnf(d269, plain, op(e2,e0) = e4 | op(e2,e0) = e1 | 'Ts8', inference(equality_resolution, [status(thm)], [d268])). % 160.72/24.14 cnf(d270, plain, e4 != e4 | op(e2,e0) = e1 | 'Ts8', inference(superposition, [status(thm)], [d269,d260])). % 160.72/24.14 cnf(d271, plain, op(e2,e0) = e1 | 'Ts8', inference(equality_resolution, [status(thm)], [d270])). % 160.72/24.14 cnf(d272, plain, op(e0,e1) = e2 | op(e0,op(e4,e0)) = e4 | 'Ts8' | 'Ts8', inference(superposition, [status(thm)], [d271,d259])). % 160.72/24.14 cnf(d273, plain, op(e1,e1) = e1 | 'Ts8', inference(superposition, [status(thm)], [d171,c26])). % 160.72/24.14 cnf(d274, plain, op(e2,e1) != e1 | 'Ts8', inference(superposition, [status(thm)], [d273,c93])). % 160.72/24.14 cnf(d275, plain, e3 != op(e3,e0) | 'Ts8', inference(superposition, [status(thm)], [d176,c126])). % 160.72/24.14 cnf(d276, plain, e4 = e3 | op(e3,e0) = e3 | op(e2,e0) = e3 | op(e4,e0) = e3 | op(e1,e0) = e3 | 'Ts8', inference(superposition, [status(thm)], [d224,c82])). % 160.72/24.14 cnf(d277, plain, op(e3,e0) = e3 | op(e2,e0) = e3 | op(e4,e0) = e3 | op(e1,e0) = e3 | 'Ts8', inference(resolution, [status(thm)], [c191,d276])). % 160.72/24.14 cnf(d278, plain, e3 != e3 | 'Ts8' | op(e2,e0) = e3 | op(e4,e0) = e3 | op(e1,e0) = e3 | 'Ts8', inference(superposition, [status(thm)], [d277,d275])). % 160.72/24.14 cnf(d279, plain, op(e2,e0) = e3 | op(e4,e0) = e3 | op(e1,e0) = e3 | 'Ts8', inference(equality_resolution, [status(thm)], [d278])). % 160.72/24.14 cnf(d280, plain, e3 = e1 | op(e2,e3) = e1 | op(e2,e1) = e1 | op(e4,e0) = e3 | op(e1,e0) = e3 | 'Ts8', inference(superposition, [status(thm)], [d279,d101])). % 160.72/24.14 cnf(d281, plain, op(e2,e3) = e1 | op(e2,e1) = e1 | op(e4,e0) = e3 | op(e1,e0) = e3 | 'Ts8', inference(resolution, [status(thm)], [c193,d280])). % 160.72/24.14 cnf(d282, plain, e1 = e0 | op(e2,e1) = e0 | 'Ts8' | op(e2,e1) = e1 | op(e4,e0) = e3 | op(e1,e0) = e3 | 'Ts8', inference(superposition, [status(thm)], [d281,d235])). % 160.72/24.14 cnf(d283, plain, op(e2,e1) = e0 | op(e2,e1) = e1 | op(e4,e0) = e3 | op(e1,e0) = e3 | 'Ts8', inference(resolution, [status(thm)], [c186,d282])). % 160.72/24.14 cnf(d284, plain, e0 != e0 | 'Ts8' | op(e2,e1) = e1 | op(e4,e0) = e3 | op(e1,e0) = e3 | 'Ts8', inference(superposition, [status(thm)], [d283,d175])). % 160.72/24.14 cnf(d285, plain, op(e2,e1) = e1 | op(e4,e0) = e3 | op(e1,e0) = e3 | 'Ts8', inference(equality_resolution, [status(thm)], [d284])). % 160.72/24.14 cnf(d286, plain, e1 != e1 | 'Ts8' | op(e4,e0) = e3 | op(e1,e0) = e3 | 'Ts8', inference(superposition, [status(thm)], [d285,d274])). % 160.72/24.14 cnf(d287, plain, op(e4,e0) = e3 | op(e1,e0) = e3 | 'Ts8', inference(equality_resolution, [status(thm)], [d286])). % 160.72/24.14 cnf(d288, plain, op(e0,e3) = e4 | op(e0,e1) = e2 | 'Ts8' | op(e1,e0) = e3 | 'Ts8', inference(superposition, [status(thm)], [d287,d272])). % 160.72/24.14 cnf(d289, plain, e4 != op(e0,e0) | op(e0,e1) = e2 | op(e1,e0) = e3 | 'Ts8', inference(superposition, [status(thm)], [d288,c112])). % 160.72/24.14 cnf(d290, plain, e4 != e4 | op(e0,e1) = e2 | op(e1,e0) = e3 | 'Ts8' | 'Ts8', inference(superposition, [status(thm)], [d224,d289])). % 160.72/24.14 cnf(d291, plain, op(e0,e1) = e2 | op(e1,e0) = e3 | 'Ts8', inference(equality_resolution, [status(thm)], [d290])). % 160.72/24.14 cnf(d292, plain, e2 = e0 | 'Ts8' | op(e1,e0) = e3 | 'Ts8', inference(superposition, [status(thm)], [d291,d174])). % 160.72/24.14 cnf(d293, plain, op(e1,e0) = e3 | 'Ts8', inference(resolution, [status(thm)], [c195,d292])). % 160.72/24.14 cnf(d294, plain, e3 != e3 | 'Ts8' | 'Ts8', inference(superposition, [status(thm)], [d293,d173])). % 160.72/24.14 cnf(d295, plain, 'Ts8', inference(equality_resolution, [status(thm)], [d294])). % 160.72/24.14 cnf(d296, plain, op(e3,e3) = e1 | 'Ts7', inference(resolution, [status(thm)], [d295,c250])). % 160.72/24.14 cnf(d297, plain, e1 != e1 | 'Ts7', inference(superposition, [status(thm)], [d296,d9])). % 160.72/24.14 cnf(d298, plain, 'Ts7', inference(equality_resolution, [status(thm)], [d297])). % 160.72/24.14 cnf(d299, plain, e0 = e2 | 'Ts6', inference(resolution, [status(thm)], [d298,d14])). % 160.72/24.14 cnf(d300, plain, e2 != e2 | 'Ts6', inference(superposition, [status(thm)], [d299,c195])). % 160.72/24.14 cnf(d301, plain, 'Ts6', inference(equality_resolution, [status(thm)], [d300])). % 160.72/24.14 cnf(d302, plain, 'Ts5', inference(resolution, [status(thm)], [d301,d11])). % 160.72/24.14 cnf(d303, plain, op(e3,e3) = e1 | 'Ts4', inference(resolution, [status(thm)], [d302,c243])). % 160.72/24.14 cnf(d304, plain, e1 != e1 | 'Ts4', inference(superposition, [status(thm)], [d303,d9])). % 160.72/24.14 cnf(d305, plain, 'Ts4', inference(equality_resolution, [status(thm)], [d304])). % 160.72/24.14 cnf(d306, plain, op(e0,e0) = e4, inference(resolution, [status(thm)], [d305,d8])). % 160.72/24.14 cnf(d307, plain, op(e4,e0) != e4, inference(demodulation, [status(thm)], [c184,d306])). % 160.72/24.14 cnf(d308, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d307,d5])). % 160.72/24.14 cnf(d309, plain, op(e3,e1) = e1 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d308,c26])). % 160.72/24.14 cnf(d310, plain, e1 != e1 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d309,d4])). % 160.72/24.14 cnf(d311, plain, unit = e2 | unit = e4 | unit = e1, inference(equality_resolution, [status(thm)], [d310])). % 160.72/24.14 cnf(d312, plain, op(e2,e2) = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d311,c33])). % 160.72/24.14 cnf(d313, plain, e4 = e2 | unit = e4 | unit = e1, inference(demodulation, [status(thm)], [d312,c198])). % 160.72/24.14 cnf(d314, plain, unit = e4 | unit = e1, inference(resolution, [status(thm)], [c190,d313])). % 160.72/24.14 cnf(d315, plain, op(e2,e4) = e2 | unit = e1, inference(superposition, [status(thm)], [d314,c33])). % 160.72/24.14 cnf(d316, plain, e3 = e2 | unit = e1, inference(demodulation, [status(thm)], [d315,d0])). % 160.72/24.14 cnf(d317, plain, unit = e1, inference(resolution, [status(thm)], [c192,d316])). % 160.72/24.14 cnf(d318, plain, op(e0,e1) = e0, inference(demodulation, [status(thm)], [c35,d317])). % 160.72/24.14 cnf(d319, plain, op(e2,e1) = e2, inference(demodulation, [status(thm)], [c33,d317])). % 160.72/24.14 cnf(d320, plain, op(e2,e0) = e0 | op(e2,e3) = e0 | e2 = e0, inference(demodulation, [status(thm)], [d82,d319])). % 160.72/24.14 cnf(d321, plain, op(e2,e0) = e0 | op(e2,e3) = e0, inference(resolution, [status(thm)], [c195,d320])). % 160.72/24.14 cnf(d322, plain, op(e1,e0) = e0, inference(demodulation, [status(thm)], [c25,d317])). % 160.72/24.14 cnf(d323, plain, op(e2,e0) != e0, inference(demodulation, [status(thm)], [c88,d322])). % 160.72/24.14 cnf(d324, plain, op(e2,e3) = e0, inference(resolution, [status(thm)], [d323,d321])). % 160.72/24.14 cnf(d325, plain, op(e2,e0) = e1 | op(e2,e3) = e1 | e2 = e1, inference(demodulation, [status(thm)], [d101,d319])). % 160.72/24.14 cnf(d326, plain, op(e2,e0) = e1 | e0 = e1 | e2 = e1, inference(demodulation, [status(thm)], [d325,d324])). % 160.72/24.14 cnf(d327, plain, op(e2,e0) = e1 | e0 = e1, inference(resolution, [status(thm)], [c188,d326])). % 160.72/24.14 cnf(d328, plain, e0 != op(e3,e4), inference(demodulation, [status(thm)], [c161,d13])). % 160.72/24.14 cnf(d329, plain, e0 != e1, inference(demodulation, [status(thm)], [d328,d3])). % 160.72/24.14 cnf(d330, plain, op(e2,e0) = e1, inference(resolution, [status(thm)], [d329,d327])). % 160.72/24.14 cnf(d331, plain, op(e0,e1) = e2 | op(e0,op(e4,e0)) = e4 | ~'Ts0', inference(demodulation, [status(thm)], [c226,d330])). % 160.72/24.14 cnf(d332, plain, op(e0,op(e4,e0)) = e4 | e0 = e2 | ~'Ts0', inference(demodulation, [status(thm)], [d331,d318])). % 160.72/24.14 cnf(d333, plain, op(e2,e3) != e2, inference(demodulation, [status(thm)], [c148,d319])). % 160.72/24.14 cnf(d334, plain, e0 != e2, inference(demodulation, [status(thm)], [d333,d324])). % 160.72/24.14 cnf(d335, plain, op(e0,op(e4,e0)) = e4 | ~'Ts0', inference(resolution, [status(thm)], [d334,d332])). % 160.72/24.14 cnf(d336, plain, op(e0,e0) = e1 | op(e3,op(e3,e0)) != e0 | 'Ts0', inference(demodulation, [status(thm)], [c201,d322])). % 160.72/24.14 cnf(d337, plain, e4 = e1 | op(e3,op(e3,e0)) != e0 | 'Ts0', inference(demodulation, [status(thm)], [d336,d306])). % 160.72/24.14 cnf(d338, plain, op(e3,op(e3,e0)) != e0 | 'Ts0', inference(resolution, [status(thm)], [c189,d337])). % 160.72/24.14 cnf(d339, plain, op(e3,e1) = e3, inference(demodulation, [status(thm)], [c32,d317])). % 160.72/24.14 cnf(d340, plain, e3 != op(e3,e0), inference(demodulation, [status(thm)], [c126,d339])). % 160.72/24.14 cnf(d341, plain, op(e1,e1) = e1, inference(demodulation, [status(thm)], [c26,d317])). % 160.72/24.14 cnf(d342, plain, op(e1,e4) = e4, inference(demodulation, [status(thm)], [c29,d317])). % 160.72/24.14 cnf(d343, plain, op(e1,e2) = e2, inference(demodulation, [status(thm)], [c27,d317])). % 160.72/24.14 cnf(d344, plain, op(e1,e3) = e3, inference(demodulation, [status(thm)], [c28,d317])). % 160.72/24.14 cnf(d345, plain, op(e0,e0) = e3 | op(e0,op(e1,e0)) = e1 | 'Ts0' | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4 | op(e3,e0) = e1, inference(superposition, [status(thm)], [c17,c203])). % 160.72/24.14 cnf(d346, plain, op(e0,e0) = e1 | op(e0,e0) = e3 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4 | op(e3,e0) = e1 | 'Ts0' | op(e1,e3) = e0 | op(e1,e2) = e0 | op(e1,e4) = e0 | op(e1,e1) = e0, inference(superposition, [status(thm)], [c41,d345])). % 160.72/24.14 cnf(d347, plain, e4 = e3 | op(e0,e0) = e1 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4 | op(e3,e0) = e1 | op(e1,e3) = e0 | op(e1,e2) = e0 | op(e1,e4) = e0 | op(e1,e1) = e0 | 'Ts0', inference(demodulation, [status(thm)], [d346,d306])). % 160.72/24.14 cnf(d348, plain, e4 = e3 | e4 = e1 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4 | op(e3,e0) = e1 | op(e1,e3) = e0 | op(e1,e2) = e0 | op(e1,e4) = e0 | op(e1,e1) = e0 | 'Ts0', inference(demodulation, [status(thm)], [d347,d306])). % 160.72/24.14 cnf(d349, plain, e4 = e3 | e4 = e1 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4 | op(e3,e0) = e1 | e3 = e0 | op(e1,e2) = e0 | op(e1,e4) = e0 | op(e1,e1) = e0 | 'Ts0', inference(demodulation, [status(thm)], [d348,d344])). % 160.72/24.14 cnf(d350, plain, e4 = e3 | e4 = e1 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4 | op(e3,e0) = e1 | e3 = e0 | e2 = e0 | op(e1,e4) = e0 | op(e1,e1) = e0 | 'Ts0', inference(demodulation, [status(thm)], [d349,d343])). % 160.72/24.14 cnf(d351, plain, e4 = e3 | e4 = e1 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4 | op(e3,e0) = e1 | e3 = e0 | e2 = e0 | e4 = e0 | op(e1,e1) = e0 | 'Ts0', inference(demodulation, [status(thm)], [d350,d342])). % 160.72/24.14 cnf(d352, plain, e4 = e3 | e4 = e1 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e4 | op(e3,e0) = e1 | e3 = e0 | e2 = e0 | e4 = e0 | e1 = e0 | 'Ts0', inference(demodulation, [status(thm)], [d351,d341])). % 160.72/24.14 cnf(d353, plain, op(e3,e0) != e4, inference(demodulation, [status(thm)], [c87,d306])). % 160.72/24.14 cnf(d354, plain, e4 = e3 | e4 = e1 | op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e1 | e3 = e0 | e2 = e0 | e4 = e0 | e1 = e0 | 'Ts0', inference(resolution, [status(thm)], [d353,d352])). % 160.72/24.14 cnf(d355, plain, op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e1 | e3 = e0 | e2 = e0 | e4 = e0 | e4 = e3 | e4 = e1 | 'Ts0', inference(resolution, [status(thm)], [c186,d354])). % 160.72/24.14 cnf(d356, plain, op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e1 | e2 = e0 | e4 = e0 | e4 = e3 | e4 = e1 | 'Ts0', inference(resolution, [status(thm)], [c187,d355])). % 160.72/24.14 cnf(d357, plain, op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e1 | e2 = e0 | e4 = e0 | e4 = e3 | 'Ts0', inference(resolution, [status(thm)], [c189,d356])). % 160.72/24.14 cnf(d358, plain, op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e1 | e2 = e0 | e4 = e0 | 'Ts0', inference(resolution, [status(thm)], [c191,d357])). % 160.72/24.14 cnf(d359, plain, op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e1 | e2 = e0 | 'Ts0', inference(resolution, [status(thm)], [c194,d358])). % 160.72/24.14 cnf(d360, plain, op(e3,e0) = e3 | op(e3,e0) = e2 | op(e3,e0) = e1 | 'Ts0', inference(resolution, [status(thm)], [c195,d359])). % 160.72/24.14 cnf(d361, plain, op(e3,e0) != e1, inference(demodulation, [status(thm)], [c182,d330])). % 160.72/24.14 cnf(d362, plain, op(e3,e0) = e3 | op(e3,e0) = e2 | 'Ts0', inference(resolution, [status(thm)], [d361,d360])). % 160.72/24.14 cnf(d363, plain, e3 != e3 | op(e3,e0) = e2 | 'Ts0', inference(superposition, [status(thm)], [d362,d340])). % 160.72/24.14 cnf(d364, plain, op(e3,e0) = e2 | 'Ts0', inference(equality_resolution, [status(thm)], [d363])). % 160.72/24.14 cnf(d365, plain, op(e3,e2) != e0 | 'Ts0' | 'Ts0', inference(superposition, [status(thm)], [d364,d338])). % 160.72/24.14 cnf(d366, plain, op(e3,e0) != e0 | op(e1,op(e1,e0)) != e0 | 'Ts0' | op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e4) = e0 | op(e3,e1) = e0, inference(superposition, [status(thm)], [c51,c200])). % 160.72/24.14 cnf(d367, plain, e0 != e0 | op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e4) = e0 | op(e3,e1) = e0 | op(e1,op(e1,e0)) != e0 | 'Ts0' | op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e4) = e0 | op(e3,e1) = e0, inference(superposition, [status(thm)], [c51,d366])). % 160.72/24.14 cnf(d368, plain, op(e3,e3) = e0 | op(e3,e2) = e0 | e1 = e0 | op(e3,e1) = e0 | op(e1,op(e1,e0)) != e0 | e0 != e0 | 'Ts0', inference(demodulation, [status(thm)], [d367,d3])). % 160.72/24.14 cnf(d369, plain, op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0 | op(e1,op(e1,e0)) != e0 | e0 != e0 | 'Ts0', inference(resolution, [status(thm)], [c186,d368])). % 160.72/24.14 cnf(d370, plain, op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0 | op(e1,e0) != e0 | e0 != e0 | 'Ts0', inference(demodulation, [status(thm)], [d369,d322])). % 160.72/24.14 cnf(d371, plain, op(e3,e3) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0 | e0 != e0 | e0 != e0 | 'Ts0', inference(demodulation, [status(thm)], [d370,d322])). % 160.72/24.14 cnf(d372, plain, op(e3,e3) = e0 | op(e3,e2) = e0 | e3 = e0 | e0 != e0 | 'Ts0', inference(demodulation, [status(thm)], [d371,d339])). % 160.72/24.14 cnf(d373, plain, op(e3,e3) = e0 | op(e3,e2) = e0 | e0 != e0 | 'Ts0', inference(resolution, [status(thm)], [c187,d372])). % 160.72/24.14 cnf(d374, plain, op(e3,e3) != e0, inference(demodulation, [status(thm)], [c167,d324])). % 160.72/24.14 cnf(d375, plain, op(e3,e2) = e0 | e0 != e0 | 'Ts0', inference(resolution, [status(thm)], [d374,d373])). % 160.72/24.14 cnf(d376, plain, op(e3,e2) = e0 | 'Ts0', inference(equality_resolution, [status(thm)], [d375])). % 160.72/24.14 cnf(d377, plain, e0 != e0 | 'Ts0' | 'Ts0', inference(superposition, [status(thm)], [d376,d365])). % 160.72/24.14 cnf(d378, plain, 'Ts0', inference(equality_resolution, [status(thm)], [d377])). % 160.72/24.14 cnf(d379, plain, op(e0,op(e4,e0)) = e4, inference(resolution, [status(thm)], [d378,d335])). % 160.72/24.14 cnf(d380, plain, op(e4,e0) = e0 | op(e4,e0) = e3 | op(e4,e0) = e2 | op(e4,e0) = e1, inference(resolution, [status(thm)], [d307,c10])). % 160.72/24.14 cnf(d381, plain, op(e4,e0) != e0, inference(demodulation, [status(thm)], [c89,d322])). % 160.72/24.14 cnf(d382, plain, op(e4,e0) = e3 | op(e4,e0) = e2 | op(e4,e0) = e1, inference(resolution, [status(thm)], [d381,d380])). % 160.72/24.14 cnf(d383, plain, op(e4,e0) != e1, inference(demodulation, [status(thm)], [c90,d330])). % 160.72/24.14 cnf(d384, plain, op(e4,e0) = e3 | op(e4,e0) = e2, inference(resolution, [status(thm)], [d383,d382])). % 160.72/24.14 cnf(d385, plain, op(e0,e3) = e4 | op(e4,e0) = e2, inference(superposition, [status(thm)], [d384,d379])). % 160.72/24.14 cnf(d386, plain, op(e0,e3) != e4, inference(demodulation, [status(thm)], [c112,d306])). % 160.72/24.14 cnf(d387, plain, op(e4,e0) = e2, inference(resolution, [status(thm)], [d386,d385])). % 160.72/24.14 cnf(d388, plain, op(e0,e2) = e4, inference(demodulation, [status(thm)], [d379,d387])). % 160.72/24.14 cnf(d389, plain, op(e0,e2) != e4, inference(demodulation, [status(thm)], [c160,d306])). % 160.72/24.14 cnf(d390, plain, $false, inference(resolution, [status(thm)], [d389,d388])). % 160.72/24.14 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------