%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG061+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 : n012.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:20 AM UTC 2026 % Result : Theorem 63.01s 8.38s % Output : CNFRefutation 63.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : ALG061+1 : TPTP v9.3.1. Released v2.7.0. % 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.03/0.30 % Computer : n012.cluster.edu % 0.03/0.30 % Model : x86_64 x86_64 % 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.03/0.30 % Memory : 8046.5625MB % 0.03/0.30 % OS : Linux 6.8.0-71-generic % 0.03/0.30 % CPULimit : 300 % 0.03/0.30 % WCLimit : 300 % 0.03/0.30 % DateTime : Sat Sep 26 21:03:49 UTC 2026 % 0.03/0.30 % CPUTime : % 0.03/0.30 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 63.01/8.38 % SZS status Theorem for theBenchmark.p % 63.01/8.38 % SZS output start CNFRefutation for theBenchmark.p % 63.01/8.38 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))))))))))))))))))))))))))))). % 63.01/8.38 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))))))))))))))). % 63.01/8.38 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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 63.01/8.38 fof(ax5, axiom, (e0 != e1 & (e0 != e2 & (e0 != e3 & (e0 != e4 & (e1 != e2 & (e1 != e3 & (e1 != e4 & (e2 != e3 & (e2 != e4 & e3 != e4)))))))))). % 63.01/8.38 fof(ax6, axiom, (e0 = op(e1,op(op(e1,e1),op(e1,e1))) & (e2 = op(op(e1,e1),op(e1,e1)) & (e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))) & e4 = op(e1,e1))))). % 63.01/8.38 fof(co1, conjecture, ~(((op(e0,e0) = e0 | (op(e1,e1) = e0 | (op(e2,e2) = e0 | (op(e3,e3) = e0 | op(e4,e4) = e0)))) & ((op(e0,e0) = e1 | (op(e1,e1) = e1 | (op(e2,e2) = e1 | (op(e3,e3) = e1 | op(e4,e4) = e1)))) & ((op(e0,e0) = e2 | (op(e1,e1) = e2 | (op(e2,e2) = e2 | (op(e3,e3) = e2 | op(e4,e4) = e2)))) & ((op(e0,e0) = e3 | (op(e1,e1) = e3 | (op(e2,e2) = e3 | (op(e3,e3) = e3 | op(e4,e4) = e3)))) & ((op(e0,e0) = e4 | (op(e1,e1) = e4 | (op(e2,e2) = e4 | (op(e3,e3) = e4 | op(e4,e4) = e4)))) & (((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)))))))))))))))). % 63.01/8.38 fof(negated_conjecture, negated_conjecture, ~~(((op(e0,e0) = e0 | (op(e1,e1) = e0 | (op(e2,e2) = e0 | (op(e3,e3) = e0 | op(e4,e4) = e0)))) & ((op(e0,e0) = e1 | (op(e1,e1) = e1 | (op(e2,e2) = e1 | (op(e3,e3) = e1 | op(e4,e4) = e1)))) & ((op(e0,e0) = e2 | (op(e1,e1) = e2 | (op(e2,e2) = e2 | (op(e3,e3) = e2 | op(e4,e4) = e2)))) & ((op(e0,e0) = e3 | (op(e1,e1) = e3 | (op(e2,e2) = e3 | (op(e3,e3) = e3 | op(e4,e4) = e3)))) & ((op(e0,e0) = e4 | (op(e1,e1) = e4 | (op(e2,e2) = e4 | (op(e3,e3) = e4 | op(e4,e4) = e4)))) & (((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))))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 63.01/8.38 cnf(c11, plain, op(e4,e2) = e3 | op(e4,e2) = e2 | op(e4,e2) = e1 | op(e4,e2) = e0 | op(e4,e2) = e4, inference(clausification, [status(esa)], [ax1])). % 63.01/8.38 cnf(c16, plain, op(e3,e2) = e4 | op(e3,e2) = e3 | op(e3,e2) = e0 | op(e3,e2) = e2 | op(e3,e2) = e1, inference(clausification, [status(esa)], [ax1])). % 63.01/8.38 cnf(c26, plain, op(unit,e1) = e1, inference(clausification, [status(esa)], [ax2])). % 63.01/8.38 cnf(c27, plain, op(unit,e2) = e2, inference(clausification, [status(esa)], [ax2])). % 63.01/8.38 cnf(c28, plain, op(unit,e3) = e3, inference(clausification, [status(esa)], [ax2])). % 63.01/8.38 cnf(c30, plain, unit = e1 | unit = e0 | unit = e4 | unit = e3 | unit = e2, inference(clausification, [status(esa)], [ax2])). % 63.01/8.38 cnf(c31, plain, op(e4,unit) = e4, inference(clausification, [status(esa)], [ax2])). % 63.01/8.38 cnf(c33, plain, op(e2,unit) = e2, inference(clausification, [status(esa)], [ax2])). % 63.01/8.38 cnf(c93, plain, op(e2,e1) != op(e1,e1), inference(clausification, [status(esa)], [ax4])). % 63.01/8.38 cnf(c99, plain, op(e4,e2) != op(e1,e2), inference(clausification, [status(esa)], [ax4])). % 63.01/8.38 cnf(c100, plain, op(e4,e2) != op(e2,e2), inference(clausification, [status(esa)], [ax4])). % 63.01/8.38 cnf(c110, plain, op(e4,e4) != op(e2,e4), inference(clausification, [status(esa)], [ax4])). % 63.01/8.38 cnf(c123, plain, op(e2,e2) != op(e2,e1), inference(clausification, [status(esa)], [ax4])). % 63.01/8.38 cnf(c125, plain, op(e2,e4) != op(e2,e2), inference(clausification, [status(esa)], [ax4])). % 63.01/8.38 cnf(c140, plain, op(e4,e2) != op(e4,e0), inference(clausification, [status(esa)], [ax4])). % 63.01/8.38 cnf(c143, plain, op(e3,e3) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 63.01/8.38 cnf(c147, plain, op(e2,e3) != op(e2,e2), inference(clausification, [status(esa)], [ax4])). % 63.01/8.38 cnf(c150, plain, op(e2,e2) != op(e2,e0), inference(clausification, [status(esa)], [ax4])). % 63.01/8.38 cnf(c185, plain, op(e2,e0) != op(e0,e0), inference(clausification, [status(esa)], [ax4])). % 63.01/8.38 cnf(c186, plain, e1 != e0, inference(clausification, [status(esa)], [ax5])). % 63.01/8.38 cnf(c187, plain, e3 != e0, inference(clausification, [status(esa)], [ax5])). % 63.01/8.38 cnf(c188, plain, e2 != e1, inference(clausification, [status(esa)], [ax5])). % 63.01/8.38 cnf(c189, plain, e4 != e1, inference(clausification, [status(esa)], [ax5])). % 63.01/8.38 cnf(c191, plain, e4 != e3, inference(clausification, [status(esa)], [ax5])). % 63.01/8.38 cnf(c192, plain, e3 != e2, inference(clausification, [status(esa)], [ax5])). % 63.01/8.38 cnf(c193, plain, e3 != e1, inference(clausification, [status(esa)], [ax5])). % 63.01/8.38 cnf(c194, plain, e4 != e0, inference(clausification, [status(esa)], [ax5])). % 63.01/8.38 cnf(c195, plain, e2 != e0, inference(clausification, [status(esa)], [ax5])). % 63.01/8.38 cnf(c196, plain, op(e1,op(op(e1,e1),op(e1,e1))) = e0, inference(clausification, [status(esa)], [ax6])). % 63.01/8.38 cnf(c197, plain, op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))) = e3, inference(clausification, [status(esa)], [ax6])). % 63.01/8.38 cnf(c198, plain, op(e1,e1) = e4, inference(clausification, [status(esa)], [ax6])). % 63.01/8.38 cnf(c199, plain, op(op(e1,e1),op(e1,e1)) = e2, inference(clausification, [status(esa)], [ax6])). % 63.01/8.38 cnf(c200, plain, op(e2,e2) = e0 | op(e4,e4) = e0 | op(e1,e1) = e0 | op(e0,e0) = e0 | op(e3,e3) = e0, inference(clausification, [status(esa)], [negated_conjecture])). % 63.01/8.38 cnf(c216, plain, X0 | op(e3,op(e3,e2)) != e2 | op(e2,op(e1,e2)) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 63.01/8.38 cnf(c218, plain, X0 | op(e2,op(e3,e2)) = e3 | op(e2,op(e1,e2)) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 63.01/8.38 cnf(c224, plain, op(e2,e2) = e1 | op(e1,e1) = e1 | op(e3,e3) = e1 | op(e0,e0) = e1 | op(e4,e4) = e1, inference(clausification, [status(esa)], [negated_conjecture])). % 63.01/8.38 cnf(c238, plain, ~X0 | op(e0,op(e0,e2)) != e2 | op(e2,op(e4,e2)) = e4, inference(clausification, [status(esa)], [negated_conjecture])). % 63.01/8.38 cnf(d0, plain, op(e4,op(e1,e1)) = e2, inference(demodulation, [status(thm)], [c199,c198])). % 63.01/8.38 cnf(d1, plain, op(e4,e4) = e2, inference(demodulation, [status(thm)], [d0,c198])). % 63.01/8.38 cnf(d2, plain, e2 != op(e2,e4), inference(demodulation, [status(thm)], [c110,d1])). % 63.01/8.38 cnf(d3, plain, op(op(e4,op(e1,e1)),op(op(e1,e1),op(e1,e1))) = e3, inference(demodulation, [status(thm)], [c197,c198])). % 63.01/8.38 cnf(d4, plain, op(op(e4,e4),op(op(e1,e1),op(e1,e1))) = e3, inference(demodulation, [status(thm)], [d3,c198])). % 63.01/8.38 cnf(d5, plain, op(op(e4,e4),op(e4,op(e1,e1))) = e3, inference(demodulation, [status(thm)], [d4,c198])). % 63.01/8.38 cnf(d6, plain, op(op(e4,e4),op(e4,e4)) = e3, inference(demodulation, [status(thm)], [d5,c198])). % 63.01/8.38 cnf(d7, plain, op(e2,op(e4,e4)) = e3, inference(demodulation, [status(thm)], [d6,d1])). % 63.01/8.38 cnf(d8, plain, op(e2,e2) = e3, inference(demodulation, [status(thm)], [d7,d1])). % 63.01/8.38 cnf(d9, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | op(e2,e2) = e0 | op(e4,e4) = e0 | e4 = e0, inference(demodulation, [status(thm)], [c200,c198])). % 63.01/8.38 cnf(d10, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | op(e2,e2) = e0 | op(e4,e4) = e0, inference(resolution, [status(thm)], [c194,d9])). % 63.01/8.38 cnf(d11, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | op(e2,e2) = e0 | e2 = e0, inference(demodulation, [status(thm)], [d10,d1])). % 63.01/8.38 cnf(d12, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | op(e2,e2) = e0, inference(resolution, [status(thm)], [c195,d11])). % 63.01/8.38 cnf(d13, plain, op(e0,e0) = e0 | op(e3,e3) = e0 | e3 = e0, inference(demodulation, [status(thm)], [d12,d8])). % 63.01/8.38 cnf(d14, plain, op(e0,e0) = e0 | op(e3,e3) = e0, inference(resolution, [status(thm)], [c187,d13])). % 63.01/8.38 cnf(d15, plain, op(e0,e0) = e1 | op(e3,e3) = e1 | op(e2,e2) = e1 | op(e4,e4) = e1 | e4 = e1, inference(demodulation, [status(thm)], [c224,c198])). % 63.01/8.38 cnf(d16, plain, op(e0,e0) = e1 | op(e3,e3) = e1 | op(e2,e2) = e1 | op(e4,e4) = e1, inference(resolution, [status(thm)], [c189,d15])). % 63.01/8.38 cnf(d17, plain, op(e0,e0) = e1 | op(e3,e3) = e1 | op(e2,e2) = e1 | e2 = e1, inference(demodulation, [status(thm)], [d16,d1])). % 63.01/8.38 cnf(d18, plain, op(e0,e0) = e1 | op(e3,e3) = e1 | op(e2,e2) = e1, inference(resolution, [status(thm)], [c188,d17])). % 63.01/8.38 cnf(d19, plain, op(e0,e0) = e1 | op(e3,e3) = e1 | e3 = e1, inference(demodulation, [status(thm)], [d18,d8])). % 63.01/8.38 cnf(d20, plain, op(e0,e0) = e1 | op(e3,e3) = e1, inference(resolution, [status(thm)], [c193,d19])). % 63.01/8.38 cnf(d21, plain, e1 = e0 | op(e3,e3) = e0 | op(e3,e3) = e1, inference(superposition, [status(thm)], [d20,d14])). % 63.01/8.38 cnf(d22, plain, op(e3,e3) = e0 | op(e3,e3) = e1, inference(resolution, [status(thm)], [c186,d21])). % 63.01/8.38 cnf(d23, plain, op(e0,e2) = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c30,c27])). % 63.01/8.38 cnf(d24, plain, op(e0,e2) != e2 | op(e2,op(e4,e2)) = e4 | ~'Ts3' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d23,c238])). % 63.01/8.38 cnf(d25, plain, e2 != e2 | op(e2,op(e4,e2)) = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | ~'Ts3' | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d23,d24])). % 63.01/8.38 cnf(d26, plain, op(e2,op(e4,e2)) = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | ~'Ts3', inference(equality_resolution, [status(thm)], [d25])). % 63.01/8.38 cnf(d27, plain, e3 != op(e2,e1), inference(demodulation, [status(thm)], [c123,d8])). % 63.01/8.38 cnf(d28, plain, e3 != op(e2,e0), inference(demodulation, [status(thm)], [c150,d8])). % 63.01/8.38 cnf(d29, plain, op(e1,op(e4,op(e1,e1))) = e0, inference(demodulation, [status(thm)], [c196,c198])). % 63.01/8.38 cnf(d30, plain, op(e1,op(e4,e4)) = e0, inference(demodulation, [status(thm)], [d29,c198])). % 63.01/8.38 cnf(d31, plain, op(e1,e2) = e0, inference(demodulation, [status(thm)], [d30,d1])). % 63.01/8.38 cnf(d32, plain, op(e2,op(e3,e2)) = e3 | op(e2,e0) = e1 | 'Ts3', inference(demodulation, [status(thm)], [c218,d31])). % 63.01/8.38 cnf(d33, plain, op(e3,op(e3,e2)) != e2 | op(e2,e0) = e1 | 'Ts3', inference(demodulation, [status(thm)], [c216,d31])). % 63.01/8.38 cnf(d34, plain, op(e2,e0) = e3 | op(e2,op(e1,e2)) = e1 | 'Ts3' | op(e3,e2) = e3 | op(e3,e2) = e2 | op(e3,e2) = e4 | op(e3,e2) = e1, inference(superposition, [status(thm)], [c16,c218])). % 63.01/8.38 cnf(d35, plain, op(e2,e3) = e3 | op(e2,op(e1,e2)) = e1 | 'Ts3' | op(e3,e2) = e2 | op(e3,e2) = e4 | op(e3,e2) = e1 | op(e2,op(e1,e2)) = e1 | op(e2,e0) = e3 | 'Ts3', inference(superposition, [status(thm)], [d34,c218])). % 63.01/8.38 cnf(d36, plain, op(e3,e2) = e2 | op(e3,e2) = e4 | op(e3,e2) = e1 | op(e2,e0) = e1 | op(e2,e0) = e3 | op(e2,e3) = e3 | 'Ts3', inference(demodulation, [status(thm)], [d35,d31])). % 63.01/8.38 cnf(d37, plain, op(e2,e3) != e3, inference(demodulation, [status(thm)], [c147,d8])). % 63.01/8.38 cnf(d38, plain, op(e3,e2) = e2 | op(e3,e2) = e4 | op(e3,e2) = e1 | op(e2,e0) = e1 | op(e2,e0) = e3 | 'Ts3', inference(resolution, [status(thm)], [d37,d36])). % 63.01/8.38 cnf(d39, plain, op(e3,e2) != e2 | op(e2,e0) = e1 | 'Ts3' | op(e3,e2) = e4 | op(e3,e2) = e1 | op(e2,e0) = e3 | op(e2,e0) = e1 | 'Ts3', inference(superposition, [status(thm)], [d38,d33])). % 63.01/8.38 cnf(d40, plain, e2 != e2 | op(e3,e2) = e4 | op(e3,e2) = e1 | op(e2,e0) = e3 | op(e2,e0) = e1 | 'Ts3' | op(e3,e2) = e4 | op(e3,e2) = e1 | op(e2,e0) = e3 | op(e2,e0) = e1 | 'Ts3', inference(superposition, [status(thm)], [d38,d39])). % 63.01/8.38 cnf(d41, plain, op(e3,e2) = e4 | op(e3,e2) = e1 | op(e2,e0) = e3 | op(e2,e0) = e1 | 'Ts3', inference(equality_resolution, [status(thm)], [d40])). % 63.01/8.38 cnf(d42, plain, op(e2,e4) = e3 | op(e2,e0) = e1 | 'Ts3' | op(e3,e2) = e1 | op(e2,e0) = e3 | op(e2,e0) = e1 | 'Ts3', inference(superposition, [status(thm)], [d41,d32])). % 63.01/8.38 cnf(d43, plain, op(e2,e4) != e3, inference(demodulation, [status(thm)], [c125,d8])). % 63.01/8.38 cnf(d44, plain, op(e3,e2) = e1 | op(e2,e0) = e3 | op(e2,e0) = e1 | 'Ts3', inference(resolution, [status(thm)], [d43,d42])). % 63.01/8.38 cnf(d45, plain, op(e2,e1) = e3 | op(e2,e0) = e1 | 'Ts3' | op(e2,e0) = e3 | op(e2,e0) = e1 | 'Ts3', inference(superposition, [status(thm)], [d44,d32])). % 63.01/8.38 cnf(d46, plain, e3 != e3 | op(e2,e0) = e1 | op(e2,e1) = e3 | 'Ts3', inference(superposition, [status(thm)], [d45,d28])). % 63.01/8.38 cnf(d47, plain, op(e2,e0) = e1 | op(e2,e1) = e3 | 'Ts3', inference(equality_resolution, [status(thm)], [d46])). % 63.01/8.38 cnf(d48, plain, e1 != op(e0,e0) | op(e2,e1) = e3 | 'Ts3', inference(superposition, [status(thm)], [d47,c185])). % 63.01/8.38 cnf(d49, plain, e1 != e1 | op(e2,e1) = e3 | 'Ts3' | op(e3,e3) = e1, inference(superposition, [status(thm)], [d20,d48])). % 63.01/8.38 cnf(d50, plain, op(e3,e3) = e1 | op(e2,e1) = e3 | 'Ts3', inference(equality_resolution, [status(thm)], [d49])). % 63.01/8.38 cnf(d51, plain, e1 != op(e3,e1) | op(e2,e1) = e3 | 'Ts3', inference(superposition, [status(thm)], [d50,c143])). % 63.01/8.38 cnf(d52, plain, op(e2,e0) = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c30,c33])). % 63.01/8.38 cnf(d53, plain, e1 = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e2,e1) = e3 | 'Ts3', inference(superposition, [status(thm)], [d47,d52])). % 63.01/8.38 cnf(d54, plain, e3 != e3 | e1 = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts3', inference(superposition, [status(thm)], [d53,d27])). % 63.01/8.38 cnf(d55, plain, e1 = e2 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts3', inference(equality_resolution, [status(thm)], [d54])). % 63.01/8.38 cnf(d56, plain, e1 != e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts3', inference(superposition, [status(thm)], [d55,c188])). % 63.01/8.38 cnf(d57, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts3', inference(equality_resolution, [status(thm)], [d56])). % 63.01/8.38 cnf(d58, plain, op(e3,e1) = e1 | unit = e2 | unit = e4 | unit = e1 | 'Ts3', inference(superposition, [status(thm)], [d57,c26])). % 63.01/8.38 cnf(d59, plain, e1 != e1 | op(e2,e1) = e3 | 'Ts3' | unit = e2 | unit = e4 | unit = e1 | 'Ts3', inference(superposition, [status(thm)], [d58,d51])). % 63.01/8.38 cnf(d60, plain, op(e2,e1) = e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts3', inference(equality_resolution, [status(thm)], [d59])). % 63.01/8.38 cnf(d61, plain, e3 != e3 | unit = e2 | unit = e4 | unit = e1 | 'Ts3', inference(superposition, [status(thm)], [d60,d27])). % 63.01/8.38 cnf(d62, plain, unit = e2 | unit = e4 | unit = e1 | 'Ts3', inference(equality_resolution, [status(thm)], [d61])). % 63.01/8.38 cnf(d63, plain, op(e2,e2) = e2 | unit = e4 | unit = e1 | 'Ts3', inference(superposition, [status(thm)], [d62,c33])). % 63.01/8.38 cnf(d64, plain, e3 = e2 | unit = e4 | unit = e1 | 'Ts3', inference(demodulation, [status(thm)], [d63,d8])). % 63.01/8.38 cnf(d65, plain, unit = e4 | unit = e1 | 'Ts3', inference(resolution, [status(thm)], [c192,d64])). % 63.01/8.38 cnf(d66, plain, op(e2,e4) = e2 | unit = e1 | 'Ts3', inference(superposition, [status(thm)], [d65,c33])). % 63.01/8.38 cnf(d67, plain, e2 != e2 | unit = e1 | 'Ts3', inference(superposition, [status(thm)], [d66,d2])). % 63.01/8.38 cnf(d68, plain, unit = e1 | 'Ts3', inference(equality_resolution, [status(thm)], [d67])). % 63.01/8.38 cnf(d69, plain, op(e1,e1) = e1 | 'Ts3', inference(superposition, [status(thm)], [d68,c26])). % 63.01/8.38 cnf(d70, plain, e4 = e1 | 'Ts3', inference(demodulation, [status(thm)], [d69,c198])). % 63.01/8.38 cnf(d71, plain, 'Ts3', inference(resolution, [status(thm)], [c189,d70])). % 63.01/8.38 cnf(d72, plain, op(e2,op(e4,e2)) = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d71,d26])). % 63.01/8.38 cnf(d73, plain, op(e4,e2) != e3, inference(demodulation, [status(thm)], [c100,d8])). % 63.01/8.38 cnf(d74, plain, op(e4,e2) = e0 | op(e4,e2) = e2 | op(e4,e2) = e4 | op(e4,e2) = e1, inference(resolution, [status(thm)], [d73,c11])). % 63.01/8.38 cnf(d75, plain, op(e4,e2) != e0, inference(demodulation, [status(thm)], [c99,d31])). % 63.01/8.38 cnf(d76, plain, op(e4,e2) = e2 | op(e4,e2) = e4 | op(e4,e2) = e1, inference(resolution, [status(thm)], [d75,d74])). % 63.01/8.38 cnf(d77, plain, op(e2,e2) = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | op(e4,e2) = e4 | op(e4,e2) = e1, inference(superposition, [status(thm)], [d76,d72])). % 63.01/8.38 cnf(d78, plain, e3 = e4 | op(e4,e2) = e4 | op(e4,e2) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(demodulation, [status(thm)], [d77,d8])). % 63.01/8.38 cnf(d79, plain, e3 != e3 | op(e4,e2) = e4 | op(e4,e2) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d78,c191])). % 63.01/8.38 cnf(d80, plain, op(e4,e2) = e4 | op(e4,e2) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(equality_resolution, [status(thm)], [d79])). % 63.01/8.38 cnf(d81, plain, e4 != op(e4,e0) | op(e4,e2) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d80,c140])). % 63.01/8.38 cnf(d82, plain, op(e4,e0) = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [c30,c31])). % 63.01/8.38 cnf(d83, plain, e4 != e4 | op(e4,e2) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d82,d81])). % 63.01/8.38 cnf(d84, plain, op(e4,e2) = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(equality_resolution, [status(thm)], [d83])). % 63.01/8.38 cnf(d85, plain, op(e2,e1) = e4 | unit = e3 | unit = e2 | unit = e4 | unit = e1 | unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d84,d72])). % 63.01/8.38 cnf(d86, plain, op(e2,e1) != e4, inference(demodulation, [status(thm)], [c93,c198])). % 63.01/8.38 cnf(d87, plain, unit = e3 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [d86,d85])). % 63.01/8.38 cnf(d88, plain, op(e3,e3) = e3 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d87,c28])). % 63.01/8.38 cnf(d89, plain, e3 = e0 | op(e3,e3) = e1 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d88,d22])). % 63.01/8.38 cnf(d90, plain, op(e3,e3) = e1 | unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c187,d89])). % 63.01/8.38 cnf(d91, plain, e3 = e1 | unit = e2 | unit = e4 | unit = e1 | unit = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d88,d90])). % 63.01/8.38 cnf(d92, plain, unit = e2 | unit = e4 | unit = e1, inference(resolution, [status(thm)], [c193,d91])). % 63.01/8.38 cnf(d93, plain, op(e2,e2) = e2 | unit = e4 | unit = e1, inference(superposition, [status(thm)], [d92,c33])). % 63.01/8.38 cnf(d94, plain, e3 = e2 | unit = e4 | unit = e1, inference(demodulation, [status(thm)], [d93,d8])). % 63.01/8.38 cnf(d95, plain, unit = e4 | unit = e1, inference(resolution, [status(thm)], [c192,d94])). % 63.01/8.38 cnf(d96, plain, op(e2,e4) = e2 | unit = e1, inference(superposition, [status(thm)], [d95,c33])). % 63.01/8.38 cnf(d97, plain, e2 != e2 | unit = e1, inference(superposition, [status(thm)], [d96,d2])). % 63.01/8.38 cnf(d98, plain, unit = e1, inference(equality_resolution, [status(thm)], [d97])). % 63.01/8.38 cnf(d99, plain, op(e1,e1) = e1, inference(demodulation, [status(thm)], [c26,d98])). % 63.01/8.38 cnf(d100, plain, e1 = e4, inference(demodulation, [status(thm)], [c198,d99])). % 63.01/8.38 cnf(d101, plain, e1 != e1, inference(demodulation, [status(thm)], [c189,d100])). % 63.01/8.38 cnf(d102, plain, $false, inference(equality_resolution, [status(thm)], [d101])). % 63.01/8.38 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------