%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : ALG045+1 : TPTP v9.3.1. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n002.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:08 AM UTC 2026 % Result : Unsatisfiable 44.42s 6.59s % Output : CNFRefutation 44.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : ALG045+1 : TPTP v9.3.1. Released v2.7.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.09/0.36 % Computer : n002.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 26 21:04:51 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 44.42/6.59 % SZS status Unsatisfiable for theBenchmark.p % 44.42/6.59 % SZS output start CNFRefutation for theBenchmark.p % 44.42/6.59 fof(ax1, axiom, ((op(e0,e0) = e0 | (op(e0,e0) = e1 | (op(e0,e0) = e2 | op(e0,e0) = e3))) & ((op(e0,e1) = e0 | (op(e0,e1) = e1 | (op(e0,e1) = e2 | op(e0,e1) = e3))) & ((op(e0,e2) = e0 | (op(e0,e2) = e1 | (op(e0,e2) = e2 | op(e0,e2) = e3))) & ((op(e0,e3) = e0 | (op(e0,e3) = e1 | (op(e0,e3) = e2 | op(e0,e3) = e3))) & ((op(e1,e0) = e0 | (op(e1,e0) = e1 | (op(e1,e0) = e2 | op(e1,e0) = e3))) & ((op(e1,e1) = e0 | (op(e1,e1) = e1 | (op(e1,e1) = e2 | op(e1,e1) = e3))) & ((op(e1,e2) = e0 | (op(e1,e2) = e1 | (op(e1,e2) = e2 | op(e1,e2) = e3))) & ((op(e1,e3) = e0 | (op(e1,e3) = e1 | (op(e1,e3) = e2 | op(e1,e3) = e3))) & ((op(e2,e0) = e0 | (op(e2,e0) = e1 | (op(e2,e0) = e2 | op(e2,e0) = e3))) & ((op(e2,e1) = e0 | (op(e2,e1) = e1 | (op(e2,e1) = e2 | op(e2,e1) = e3))) & ((op(e2,e2) = e0 | (op(e2,e2) = e1 | (op(e2,e2) = e2 | op(e2,e2) = e3))) & ((op(e2,e3) = e0 | (op(e2,e3) = e1 | (op(e2,e3) = e2 | op(e2,e3) = e3))) & ((op(e3,e0) = e0 | (op(e3,e0) = e1 | (op(e3,e0) = e2 | op(e3,e0) = e3))) & ((op(e3,e1) = e0 | (op(e3,e1) = e1 | (op(e3,e1) = e2 | op(e3,e1) = e3))) & ((op(e3,e2) = e0 | (op(e3,e2) = e1 | (op(e3,e2) = e2 | op(e3,e2) = e3))) & (op(e3,e3) = e0 | (op(e3,e3) = e1 | (op(e3,e3) = e2 | op(e3,e3) = e3))))))))))))))))))). % 44.42/6.59 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 & (unit = e0 | (unit = e1 | (unit = e2 | unit = e3)))))))))))). % 44.42/6.59 fof(ax3, axiom, ((op(e0,e0) = e0 | (op(e0,e1) = e0 | (op(e0,e2) = e0 | op(e0,e3) = e0))) & ((op(e0,e0) = e0 | (op(e1,e0) = e0 | (op(e2,e0) = e0 | op(e3,e0) = e0))) & ((op(e0,e0) = e1 | (op(e0,e1) = e1 | (op(e0,e2) = e1 | op(e0,e3) = e1))) & ((op(e0,e0) = e1 | (op(e1,e0) = e1 | (op(e2,e0) = e1 | op(e3,e0) = e1))) & ((op(e0,e0) = e2 | (op(e0,e1) = e2 | (op(e0,e2) = e2 | op(e0,e3) = e2))) & ((op(e0,e0) = e2 | (op(e1,e0) = e2 | (op(e2,e0) = e2 | op(e3,e0) = e2))) & ((op(e0,e0) = e3 | (op(e0,e1) = e3 | (op(e0,e2) = e3 | op(e0,e3) = e3))) & ((op(e0,e0) = e3 | (op(e1,e0) = e3 | (op(e2,e0) = e3 | op(e3,e0) = e3))) & ((op(e1,e0) = e0 | (op(e1,e1) = e0 | (op(e1,e2) = e0 | op(e1,e3) = e0))) & ((op(e0,e1) = e0 | (op(e1,e1) = e0 | (op(e2,e1) = e0 | op(e3,e1) = e0))) & ((op(e1,e0) = e1 | (op(e1,e1) = e1 | (op(e1,e2) = e1 | op(e1,e3) = e1))) & ((op(e0,e1) = e1 | (op(e1,e1) = e1 | (op(e2,e1) = e1 | op(e3,e1) = e1))) & ((op(e1,e0) = e2 | (op(e1,e1) = e2 | (op(e1,e2) = e2 | op(e1,e3) = e2))) & ((op(e0,e1) = e2 | (op(e1,e1) = e2 | (op(e2,e1) = e2 | op(e3,e1) = e2))) & ((op(e1,e0) = e3 | (op(e1,e1) = e3 | (op(e1,e2) = e3 | op(e1,e3) = e3))) & ((op(e0,e1) = e3 | (op(e1,e1) = e3 | (op(e2,e1) = e3 | op(e3,e1) = e3))) & ((op(e2,e0) = e0 | (op(e2,e1) = e0 | (op(e2,e2) = e0 | op(e2,e3) = e0))) & ((op(e0,e2) = e0 | (op(e1,e2) = e0 | (op(e2,e2) = e0 | op(e3,e2) = e0))) & ((op(e2,e0) = e1 | (op(e2,e1) = e1 | (op(e2,e2) = e1 | op(e2,e3) = e1))) & ((op(e0,e2) = e1 | (op(e1,e2) = e1 | (op(e2,e2) = e1 | op(e3,e2) = e1))) & ((op(e2,e0) = e2 | (op(e2,e1) = e2 | (op(e2,e2) = e2 | op(e2,e3) = e2))) & ((op(e0,e2) = e2 | (op(e1,e2) = e2 | (op(e2,e2) = e2 | op(e3,e2) = e2))) & ((op(e2,e0) = e3 | (op(e2,e1) = e3 | (op(e2,e2) = e3 | op(e2,e3) = e3))) & ((op(e0,e2) = e3 | (op(e1,e2) = e3 | (op(e2,e2) = e3 | op(e3,e2) = e3))) & ((op(e3,e0) = e0 | (op(e3,e1) = e0 | (op(e3,e2) = e0 | op(e3,e3) = e0))) & ((op(e0,e3) = e0 | (op(e1,e3) = e0 | (op(e2,e3) = e0 | op(e3,e3) = e0))) & ((op(e3,e0) = e1 | (op(e3,e1) = e1 | (op(e3,e2) = e1 | op(e3,e3) = e1))) & ((op(e0,e3) = e1 | (op(e1,e3) = e1 | (op(e2,e3) = e1 | op(e3,e3) = e1))) & ((op(e3,e0) = e2 | (op(e3,e1) = e2 | (op(e3,e2) = e2 | op(e3,e3) = e2))) & ((op(e0,e3) = e2 | (op(e1,e3) = e2 | (op(e2,e3) = e2 | op(e3,e3) = e2))) & ((op(e3,e0) = e3 | (op(e3,e1) = e3 | (op(e3,e2) = e3 | op(e3,e3) = e3))) & (op(e0,e3) = e3 | (op(e1,e3) = e3 | (op(e2,e3) = e3 | op(e3,e3) = e3))))))))))))))))))))))))))))))))))). % 44.42/6.59 fof(ax4, axiom, (op(e0,e0) != op(e1,e0) & (op(e0,e0) != op(e2,e0) & (op(e0,e0) != op(e3,e0) & (op(e1,e0) != op(e2,e0) & (op(e1,e0) != op(e3,e0) & (op(e2,e0) != op(e3,e0) & (op(e0,e1) != op(e1,e1) & (op(e0,e1) != op(e2,e1) & (op(e0,e1) != op(e3,e1) & (op(e1,e1) != op(e2,e1) & (op(e1,e1) != op(e3,e1) & (op(e2,e1) != op(e3,e1) & (op(e0,e2) != op(e1,e2) & (op(e0,e2) != op(e2,e2) & (op(e0,e2) != op(e3,e2) & (op(e1,e2) != op(e2,e2) & (op(e1,e2) != op(e3,e2) & (op(e2,e2) != op(e3,e2) & (op(e0,e3) != op(e1,e3) & (op(e0,e3) != op(e2,e3) & (op(e0,e3) != op(e3,e3) & (op(e1,e3) != op(e2,e3) & (op(e1,e3) != op(e3,e3) & (op(e2,e3) != op(e3,e3) & (op(e0,e0) != op(e0,e1) & (op(e0,e0) != op(e0,e2) & (op(e0,e0) != op(e0,e3) & (op(e0,e1) != op(e0,e2) & (op(e0,e1) != op(e0,e3) & (op(e0,e2) != op(e0,e3) & (op(e1,e0) != op(e1,e1) & (op(e1,e0) != op(e1,e2) & (op(e1,e0) != op(e1,e3) & (op(e1,e1) != op(e1,e2) & (op(e1,e1) != op(e1,e3) & (op(e1,e2) != op(e1,e3) & (op(e2,e0) != op(e2,e1) & (op(e2,e0) != op(e2,e2) & (op(e2,e0) != op(e2,e3) & (op(e2,e1) != op(e2,e2) & (op(e2,e1) != op(e2,e3) & (op(e2,e2) != op(e2,e3) & (op(e3,e0) != op(e3,e1) & (op(e3,e0) != op(e3,e2) & (op(e3,e0) != op(e3,e3) & (op(e3,e1) != op(e3,e2) & (op(e3,e1) != op(e3,e3) & op(e3,e2) != op(e3,e3))))))))))))))))))))))))))))))))))))))))))))))))). % 44.42/6.59 fof(ax5, axiom, (e0 != e1 & (e0 != e2 & (e0 != e3 & (e1 != e2 & (e1 != e3 & e2 != e3)))))). % 44.42/6.59 fof(ax6, axiom, ((op(e0,e0) = e0 & (op(e1,e1) = e0 & (op(e2,e2) = e0 & op(e3,e3) = e0))) | ((op(e0,e0) = e1 & (op(e1,e1) = e1 & (op(e2,e2) = e1 & op(e3,e3) = e1))) | ((op(e0,e0) = e2 & (op(e1,e1) = e2 & (op(e2,e2) = e2 & op(e3,e3) = e2))) | (op(e0,e0) = e3 & (op(e1,e1) = e3 & (op(e2,e2) = e3 & op(e3,e3) = e3))))))). % 44.42/6.59 fof(ax9, axiom, ~((e0 = op(e2,e2) & e1 = op(e3,e2)))). % 44.42/6.59 fof(ax16, axiom, ~((e1 = op(e2,e2) & e3 = op(e0,e2)))). % 44.42/6.59 fof(ax21, axiom, ~((e2 = op(e1,e1) & e0 = op(e3,e1)))). % 44.42/6.59 fof(ax30, axiom, ~((e3 = op(e2,e2) & e1 = op(e0,e2)))). % 44.42/6.59 cnf(c2, plain, op(e0,e2) = e0 | op(e0,e2) = e1 | op(e0,e2) = e2 | op(e0,e2) = e3, inference(clausification, [status(esa)], [ax1])). % 44.42/6.59 cnf(c16, plain, op(unit,e0) = e0, inference(clausification, [status(esa)], [ax2])). % 44.42/6.59 cnf(c17, plain, op(e0,unit) = e0, inference(clausification, [status(esa)], [ax2])). % 44.42/6.59 cnf(c18, plain, op(unit,e1) = e1, inference(clausification, [status(esa)], [ax2])). % 44.42/6.59 cnf(c19, plain, op(e1,unit) = e1, inference(clausification, [status(esa)], [ax2])). % 44.42/6.59 cnf(c20, plain, op(unit,e2) = e2, inference(clausification, [status(esa)], [ax2])). % 44.42/6.59 cnf(c21, plain, op(e2,unit) = e2, inference(clausification, [status(esa)], [ax2])). % 44.42/6.59 cnf(c23, plain, op(e3,unit) = e3, inference(clausification, [status(esa)], [ax2])). % 44.42/6.59 cnf(c24, plain, unit = e0 | unit = e1 | unit = e2 | unit = e3, inference(clausification, [status(esa)], [ax2])). % 44.42/6.59 cnf(c49, plain, op(e3,e0) = e0 | op(e3,e1) = e0 | op(e3,e2) = e0 | op(e3,e3) = e0, inference(clausification, [status(esa)], [ax3])). % 44.42/6.59 cnf(c51, plain, op(e3,e0) = e1 | op(e3,e1) = e1 | op(e3,e2) = e1 | op(e3,e3) = e1, inference(clausification, [status(esa)], [ax3])). % 44.42/6.59 cnf(c62, plain, op(e2,e0) != op(e3,e0), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c63, plain, op(e0,e1) != op(e1,e1), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c65, plain, op(e0,e1) != op(e3,e1), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c69, plain, op(e0,e2) != op(e1,e2), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c70, plain, op(e0,e2) != op(e2,e2), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c71, plain, op(e0,e2) != op(e3,e2), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c72, plain, op(e1,e2) != op(e2,e2), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c77, plain, op(e0,e3) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c79, plain, op(e1,e3) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c80, plain, op(e2,e3) != op(e3,e3), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c84, plain, op(e0,e1) != op(e0,e2), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c86, plain, op(e0,e2) != op(e0,e3), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c87, plain, op(e1,e0) != op(e1,e1), inference(clausification, [status(esa)], [ax4])). % 44.42/6.59 cnf(c105, plain, e0 != e1, inference(clausification, [status(esa)], [ax5])). % 44.42/6.59 cnf(c106, plain, e0 != e2, inference(clausification, [status(esa)], [ax5])). % 44.42/6.59 cnf(c107, plain, e0 != e3, inference(clausification, [status(esa)], [ax5])). % 44.42/6.59 cnf(c108, plain, e1 != e2, inference(clausification, [status(esa)], [ax5])). % 44.42/6.59 cnf(c109, plain, e1 != e3, inference(clausification, [status(esa)], [ax5])). % 44.42/6.59 cnf(c110, plain, e2 != e3, inference(clausification, [status(esa)], [ax5])). % 44.42/6.59 cnf(c111, plain, X0 | X1 | X2 | op(e0,e0) = e3, inference(clausification, [status(esa)], [ax6])). % 44.42/6.59 cnf(c112, plain, X0 | X1 | X2 | op(e1,e1) = e3, inference(clausification, [status(esa)], [ax6])). % 44.42/6.59 cnf(c113, plain, X0 | X1 | X2 | op(e2,e2) = e3, inference(clausification, [status(esa)], [ax6])). % 44.42/6.59 cnf(c115, plain, ~X0 | op(e0,e0) = e2, inference(clausification, [status(esa)], [ax6])). % 44.42/6.59 cnf(c116, plain, ~X0 | op(e1,e1) = e2, inference(clausification, [status(esa)], [ax6])). % 44.42/6.59 cnf(c118, plain, ~X0 | op(e3,e3) = e2, inference(clausification, [status(esa)], [ax6])). % 44.42/6.59 cnf(c120, plain, ~X0 | op(e1,e1) = e1, inference(clausification, [status(esa)], [ax6])). % 44.42/6.59 cnf(c121, plain, ~X0 | op(e2,e2) = e1, inference(clausification, [status(esa)], [ax6])). % 44.42/6.59 cnf(c122, plain, ~X0 | op(e3,e3) = e1, inference(clausification, [status(esa)], [ax6])). % 44.42/6.59 cnf(c124, plain, ~X0 | op(e1,e1) = e0, inference(clausification, [status(esa)], [ax6])). % 44.42/6.59 cnf(c125, plain, ~X0 | op(e2,e2) = e0, inference(clausification, [status(esa)], [ax6])). % 44.42/6.59 cnf(c126, plain, ~X0 | op(e3,e3) = e0, inference(clausification, [status(esa)], [ax6])). % 44.42/6.59 cnf(c129, plain, e0 != op(e2,e2) | e1 != op(e3,e2), inference(clausification, [status(esa)], [ax9])). % 44.42/6.59 cnf(c136, plain, e1 != op(e2,e2) | e3 != op(e0,e2), inference(clausification, [status(esa)], [ax16])). % 44.42/6.59 cnf(c141, plain, e2 != op(e1,e1) | e0 != op(e3,e1), inference(clausification, [status(esa)], [ax21])). % 44.42/6.59 cnf(c150, plain, e3 != op(e2,e2) | e1 != op(e0,e2), inference(clausification, [status(esa)], [ax30])). % 44.42/6.59 cnf(d0, plain, op(e1,e3) != e1 | ~'Ts1', inference(superposition, [status(thm)], [c122,c79])). % 44.42/6.59 cnf(d1, plain, op(e1,e3) = e1 | unit = e0 | unit = e2 | unit = e1, inference(superposition, [status(thm)], [c24,c19])). % 44.42/6.59 cnf(d2, plain, e1 != e1 | ~'Ts1' | unit = e0 | unit = e2 | unit = e1, inference(superposition, [status(thm)], [d1,d0])). % 44.42/6.59 cnf(d3, plain, unit = e0 | unit = e2 | unit = e1 | ~'Ts1', inference(equality_resolution, [status(thm)], [d2])). % 44.42/6.59 cnf(d4, plain, op(e0,e1) = e0 | unit = e0 | unit = e2 | ~'Ts1', inference(superposition, [status(thm)], [d3,c17])). % 44.42/6.59 cnf(d5, plain, e0 != op(e0,e2) | unit = e0 | unit = e2 | ~'Ts1', inference(superposition, [status(thm)], [d4,c84])). % 44.42/6.59 cnf(d6, plain, op(e2,e3) != e2 | ~'Ts0', inference(superposition, [status(thm)], [c118,c80])). % 44.42/6.59 cnf(d7, plain, op(e2,e3) = e2 | unit = e0 | unit = e2 | unit = e1, inference(superposition, [status(thm)], [c24,c21])). % 44.42/6.59 cnf(d8, plain, e2 != e2 | ~'Ts0' | unit = e0 | unit = e2 | unit = e1, inference(superposition, [status(thm)], [d7,d6])). % 44.42/6.59 cnf(d9, plain, unit = e0 | unit = e2 | unit = e1 | ~'Ts0', inference(equality_resolution, [status(thm)], [d8])). % 44.42/6.59 cnf(d10, plain, op(e1,e1) = e1 | unit = e0 | unit = e2 | ~'Ts0', inference(superposition, [status(thm)], [d9,c19])). % 44.42/6.59 cnf(d11, plain, e1 = e2 | ~'Ts0' | unit = e0 | unit = e2 | ~'Ts0', inference(superposition, [status(thm)], [d10,c116])). % 44.42/6.59 cnf(d12, plain, unit = e0 | unit = e2 | ~'Ts0', inference(resolution, [status(thm)], [c108,d11])). % 44.42/6.59 cnf(d13, plain, op(e3,e2) = e3 | unit = e0 | ~'Ts0', inference(superposition, [status(thm)], [d12,c23])). % 44.42/6.59 cnf(d14, plain, e2 != e2 | e0 != op(e3,e1) | ~'Ts0', inference(superposition, [status(thm)], [c116,c141])). % 44.42/6.59 cnf(d15, plain, e0 = e2 | ~'Ts0' | op(e3,e0) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0, inference(superposition, [status(thm)], [c49,c118])). % 44.42/6.59 cnf(d16, plain, op(e3,e0) = e0 | op(e3,e2) = e0 | op(e3,e1) = e0 | ~'Ts0', inference(resolution, [status(thm)], [c106,d15])). % 44.42/6.59 cnf(d17, plain, e0 != e0 | e2 != e2 | ~'Ts0' | op(e3,e0) = e0 | op(e3,e2) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d16,d14])). % 44.42/6.59 cnf(d18, plain, op(e3,e0) = e0 | op(e3,e2) = e0 | e0 != e0 | ~'Ts0', inference(equality_resolution, [status(thm)], [d17])). % 44.42/6.60 cnf(d19, plain, op(e3,e0) = e0 | op(e3,e2) = e0 | ~'Ts0', inference(equality_resolution, [status(thm)], [d18])). % 44.42/6.60 cnf(d20, plain, e0 = e3 | unit = e0 | ~'Ts0' | op(e3,e0) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d19,d13])). % 44.42/6.60 cnf(d21, plain, op(e3,e0) = e0 | unit = e0 | ~'Ts0', inference(resolution, [status(thm)], [c107,d20])). % 44.42/6.60 cnf(d22, plain, op(e2,e0) != e0 | unit = e0 | ~'Ts0', inference(superposition, [status(thm)], [d21,c62])). % 44.42/6.60 cnf(d23, plain, op(e2,e0) = e0 | unit = e0 | ~'Ts0', inference(superposition, [status(thm)], [d12,c16])). % 44.42/6.60 cnf(d24, plain, e0 != e0 | unit = e0 | ~'Ts0' | unit = e0 | ~'Ts0', inference(superposition, [status(thm)], [d23,d22])). % 44.42/6.60 cnf(d25, plain, unit = e0 | ~'Ts0', inference(equality_resolution, [status(thm)], [d24])). % 44.42/6.60 cnf(d26, plain, op(e0,e0) = e0 | ~'Ts0', inference(superposition, [status(thm)], [d25,c17])). % 44.42/6.60 cnf(d27, plain, e0 = e2 | ~'Ts0' | ~'Ts0', inference(superposition, [status(thm)], [d26,c115])). % 44.42/6.60 cnf(d28, plain, ~'Ts0', inference(resolution, [status(thm)], [c106,d27])). % 44.42/6.60 cnf(d29, plain, op(e0,e0) = e3 | 'Ts2' | 'Ts1', inference(resolution, [status(thm)], [d28,c111])). % 44.42/6.60 cnf(d30, plain, op(e0,e2) != e0 | ~'Ts2', inference(superposition, [status(thm)], [c125,c70])). % 44.42/6.60 cnf(d31, plain, op(e0,e1) != e0 | ~'Ts2', inference(superposition, [status(thm)], [c124,c63])). % 44.42/6.60 cnf(d32, plain, op(e0,e3) != e0 | ~'Ts2', inference(superposition, [status(thm)], [c126,c77])). % 44.42/6.60 cnf(d33, plain, op(e0,e3) = e0 | unit = e0 | unit = e2 | unit = e1, inference(superposition, [status(thm)], [c24,c17])). % 44.42/6.60 cnf(d34, plain, e0 != e0 | ~'Ts2' | unit = e0 | unit = e2 | unit = e1, inference(superposition, [status(thm)], [d33,d32])). % 44.42/6.60 cnf(d35, plain, unit = e0 | unit = e2 | unit = e1 | ~'Ts2', inference(equality_resolution, [status(thm)], [d34])). % 44.42/6.60 cnf(d36, plain, op(e0,e1) = e0 | unit = e0 | unit = e2 | ~'Ts2', inference(superposition, [status(thm)], [d35,c17])). % 44.42/6.60 cnf(d37, plain, e0 != e0 | ~'Ts2' | unit = e0 | unit = e2 | ~'Ts2', inference(superposition, [status(thm)], [d36,d31])). % 44.42/6.60 cnf(d38, plain, unit = e0 | unit = e2 | ~'Ts2', inference(equality_resolution, [status(thm)], [d37])). % 44.42/6.60 cnf(d39, plain, op(e0,e2) = e0 | unit = e0 | ~'Ts2', inference(superposition, [status(thm)], [d38,c17])). % 44.42/6.60 cnf(d40, plain, e0 != e0 | ~'Ts2' | unit = e0 | ~'Ts2', inference(superposition, [status(thm)], [d39,d30])). % 44.42/6.60 cnf(d41, plain, unit = e0 | ~'Ts2', inference(equality_resolution, [status(thm)], [d40])). % 44.42/6.60 cnf(d42, plain, op(e3,e0) = e3 | ~'Ts2', inference(superposition, [status(thm)], [d41,c23])). % 44.42/6.60 cnf(d43, plain, e0 = e1 | op(e3,e0) = e1 | op(e3,e2) = e1 | op(e3,e1) = e1 | ~'Ts2', inference(superposition, [status(thm)], [c126,c51])). % 44.42/6.60 cnf(d44, plain, op(e3,e0) = e1 | op(e3,e2) = e1 | op(e3,e1) = e1 | ~'Ts2', inference(resolution, [status(thm)], [c105,d43])). % 44.42/6.60 cnf(d45, plain, op(e0,e1) != e1 | op(e3,e0) = e1 | op(e3,e2) = e1 | ~'Ts2', inference(superposition, [status(thm)], [d44,c65])). % 44.42/6.60 cnf(d46, plain, op(e0,e1) = e1 | ~'Ts2', inference(superposition, [status(thm)], [d41,c18])). % 44.42/6.60 cnf(d47, plain, e1 != e1 | op(e3,e0) = e1 | op(e3,e2) = e1 | ~'Ts2' | ~'Ts2', inference(superposition, [status(thm)], [d46,d45])). % 44.42/6.60 cnf(d48, plain, op(e3,e0) = e1 | op(e3,e2) = e1 | ~'Ts2', inference(equality_resolution, [status(thm)], [d47])). % 44.42/6.60 cnf(d49, plain, e1 != e1 | e0 != op(e2,e2) | op(e3,e0) = e1 | ~'Ts2', inference(superposition, [status(thm)], [d48,c129])). % 44.42/6.60 cnf(d50, plain, e0 != e0 | op(e3,e0) = e1 | e1 != e1 | ~'Ts2' | ~'Ts2', inference(superposition, [status(thm)], [c125,d49])). % 44.42/6.60 cnf(d51, plain, op(e3,e0) = e1 | e0 != e0 | ~'Ts2', inference(equality_resolution, [status(thm)], [d50])). % 44.42/6.60 cnf(d52, plain, op(e3,e0) = e1 | ~'Ts2', inference(equality_resolution, [status(thm)], [d51])). % 44.42/6.60 cnf(d53, plain, e1 = e3 | ~'Ts2' | ~'Ts2', inference(superposition, [status(thm)], [d52,d42])). % 44.42/6.60 cnf(d54, plain, ~'Ts2', inference(resolution, [status(thm)], [c109,d53])). % 44.42/6.60 cnf(d55, plain, op(e0,e0) = e3 | 'Ts1', inference(resolution, [status(thm)], [d54,d29])). % 44.42/6.60 cnf(d56, plain, op(e2,e2) = e3 | 'Ts2' | 'Ts1', inference(resolution, [status(thm)], [d28,c113])). % 44.42/6.60 cnf(d57, plain, op(e2,e2) = e3 | 'Ts1', inference(resolution, [status(thm)], [d54,d56])). % 44.42/6.60 cnf(d58, plain, op(e1,e1) = e3 | 'Ts2' | 'Ts1', inference(resolution, [status(thm)], [d28,c112])). % 44.42/6.60 cnf(d59, plain, op(e1,e1) = e3 | 'Ts1', inference(resolution, [status(thm)], [d54,d58])). % 44.42/6.60 cnf(d60, plain, op(e0,e2) != e0 | unit = e0 | unit = e2 | unit = e1, inference(superposition, [status(thm)], [d33,c86])). % 44.42/6.60 cnf(d61, plain, op(e3,e2) = e2 | unit = e0 | unit = e2 | unit = e1, inference(superposition, [status(thm)], [c24,c20])). % 44.42/6.60 cnf(d62, plain, op(e0,e2) != e2 | unit = e0 | unit = e2 | unit = e1, inference(superposition, [status(thm)], [d61,c71])). % 44.42/6.60 cnf(d63, plain, e3 != e3 | e1 != op(e0,e2) | 'Ts0' | 'Ts2' | 'Ts1', inference(superposition, [status(thm)], [c113,c150])). % 44.42/6.60 cnf(d64, plain, e1 != op(e0,e2) | e3 != e3 | 'Ts2' | 'Ts1', inference(resolution, [status(thm)], [d28,d63])). % 44.42/6.60 cnf(d65, plain, e1 != op(e0,e2) | e3 != e3 | 'Ts1', inference(resolution, [status(thm)], [d54,d64])). % 44.42/6.60 cnf(d66, plain, op(e0,e2) != e3 | 'Ts0' | 'Ts2' | 'Ts1', inference(superposition, [status(thm)], [c113,c70])). % 44.42/6.60 cnf(d67, plain, e3 != e3 | 'Ts0' | 'Ts2' | 'Ts1' | op(e0,e2) = e0 | op(e0,e2) = e2 | op(e0,e2) = e1, inference(superposition, [status(thm)], [c2,d66])). % 44.42/6.60 cnf(d68, plain, op(e0,e2) = e0 | op(e0,e2) = e2 | op(e0,e2) = e1 | e3 != e3 | 'Ts2' | 'Ts1', inference(resolution, [status(thm)], [d28,d67])). % 44.42/6.60 cnf(d69, plain, op(e0,e2) = e0 | op(e0,e2) = e2 | op(e0,e2) = e1 | e3 != e3 | 'Ts1', inference(resolution, [status(thm)], [d54,d68])). % 44.42/6.60 cnf(d70, plain, op(e0,e2) = e0 | op(e0,e2) = e2 | op(e0,e2) = e1 | 'Ts1', inference(equality_resolution, [status(thm)], [d69])). % 44.42/6.60 cnf(d71, plain, e1 != e1 | e3 != e3 | 'Ts1' | op(e0,e2) = e0 | op(e0,e2) = e2 | 'Ts1', inference(superposition, [status(thm)], [d70,d65])). % 44.42/6.60 cnf(d72, plain, op(e0,e2) = e0 | op(e0,e2) = e2 | e1 != e1 | 'Ts1', inference(equality_resolution, [status(thm)], [d71])). % 44.42/6.60 cnf(d73, plain, op(e0,e2) = e0 | op(e0,e2) = e2 | 'Ts1', inference(equality_resolution, [status(thm)], [d72])). % 44.42/6.60 cnf(d74, plain, e2 != e2 | unit = e0 | unit = e2 | unit = e1 | op(e0,e2) = e0 | 'Ts1', inference(superposition, [status(thm)], [d73,d62])). % 44.42/6.60 cnf(d75, plain, op(e0,e2) = e0 | unit = e0 | unit = e2 | unit = e1 | 'Ts1', inference(equality_resolution, [status(thm)], [d74])). % 44.42/6.60 cnf(d76, plain, e0 != e0 | unit = e0 | unit = e2 | unit = e1 | unit = e0 | unit = e2 | unit = e1 | 'Ts1', inference(superposition, [status(thm)], [d75,d60])). % 44.42/6.60 cnf(d77, plain, unit = e0 | unit = e2 | unit = e1 | 'Ts1', inference(equality_resolution, [status(thm)], [d76])). % 44.42/6.60 cnf(d78, plain, op(e1,e1) = e1 | unit = e0 | unit = e2 | 'Ts1', inference(superposition, [status(thm)], [d77,c19])). % 44.42/6.60 cnf(d79, plain, e1 = e3 | 'Ts1' | unit = e0 | unit = e2 | 'Ts1', inference(superposition, [status(thm)], [d78,d59])). % 44.42/6.60 cnf(d80, plain, unit = e0 | unit = e2 | 'Ts1', inference(resolution, [status(thm)], [c109,d79])). % 44.42/6.60 cnf(d81, plain, op(e2,e2) = e2 | unit = e0 | 'Ts1', inference(superposition, [status(thm)], [d80,c21])). % 44.42/6.60 cnf(d82, plain, e2 = e3 | 'Ts1' | unit = e0 | 'Ts1', inference(superposition, [status(thm)], [d81,d57])). % 44.42/6.60 cnf(d83, plain, unit = e0 | 'Ts1', inference(resolution, [status(thm)], [c110,d82])). % 44.42/6.60 cnf(d84, plain, op(e0,e0) = e0 | 'Ts1', inference(superposition, [status(thm)], [d83,c17])). % 44.42/6.60 cnf(d85, plain, e0 = e3 | 'Ts1' | 'Ts1', inference(superposition, [status(thm)], [d84,d55])). % 44.42/6.60 cnf(d86, plain, 'Ts1', inference(resolution, [status(thm)], [c107,d85])). % 44.42/6.60 cnf(d87, plain, e0 != op(e0,e2) | unit = e0 | unit = e2, inference(resolution, [status(thm)], [d86,d5])). % 44.42/6.60 cnf(d88, plain, op(e1,e2) = e2 | unit = e0 | unit = e2 | ~'Ts1', inference(superposition, [status(thm)], [d3,c20])). % 44.42/6.60 cnf(d89, plain, op(e0,e2) != e2 | unit = e0 | unit = e2 | ~'Ts1', inference(superposition, [status(thm)], [d88,c69])). % 44.42/6.60 cnf(d90, plain, op(e0,e2) != e2 | unit = e0 | unit = e2, inference(resolution, [status(thm)], [d86,d89])). % 44.42/6.60 cnf(d91, plain, op(e2,e2) = e1, inference(resolution, [status(thm)], [d86,c121])). % 44.42/6.60 cnf(d92, plain, e1 != e1 | e3 != op(e0,e2), inference(demodulation, [status(thm)], [c136,d91])). % 44.42/6.60 cnf(d93, plain, op(e0,e2) != e1 | ~'Ts1', inference(superposition, [status(thm)], [c121,c70])). % 44.42/6.60 cnf(d94, plain, op(e0,e2) != e1, inference(resolution, [status(thm)], [d86,d93])). % 44.42/6.60 cnf(d95, plain, op(e0,e2) = e0 | op(e0,e2) = e2 | op(e0,e2) = e3, inference(resolution, [status(thm)], [d94,c2])). % 44.42/6.60 cnf(d96, plain, e3 != e3 | e1 != e1 | op(e0,e2) = e0 | op(e0,e2) = e2, inference(superposition, [status(thm)], [d95,d92])). % 44.42/6.60 cnf(d97, plain, op(e0,e2) = e0 | op(e0,e2) = e2 | e1 != e1, inference(equality_resolution, [status(thm)], [d96])). % 44.42/6.60 cnf(d98, plain, op(e0,e2) = e0 | op(e0,e2) = e2, inference(equality_resolution, [status(thm)], [d97])). % 44.42/6.60 cnf(d99, plain, e2 != e2 | unit = e0 | unit = e2 | op(e0,e2) = e0, inference(superposition, [status(thm)], [d98,d90])). % 44.42/6.60 cnf(d100, plain, op(e0,e2) = e0 | unit = e0 | unit = e2, inference(equality_resolution, [status(thm)], [d99])). % 44.42/6.60 cnf(d101, plain, e0 != e0 | unit = e0 | unit = e2 | unit = e0 | unit = e2, inference(superposition, [status(thm)], [d100,d87])). % 44.42/6.60 cnf(d102, plain, unit = e0 | unit = e2, inference(equality_resolution, [status(thm)], [d101])). % 44.42/6.60 cnf(d103, plain, op(e1,e2) = e1 | unit = e0, inference(superposition, [status(thm)], [d102,c19])). % 44.42/6.60 cnf(d104, plain, op(e1,e2) != e1, inference(demodulation, [status(thm)], [c72,d91])). % 44.42/6.60 cnf(d105, plain, unit = e0, inference(resolution, [status(thm)], [d104,d103])). % 44.42/6.60 cnf(d106, plain, op(e1,e0) = e1, inference(demodulation, [status(thm)], [c19,d105])). % 44.42/6.60 cnf(d107, plain, op(e1,e0) != e1 | ~'Ts1', inference(superposition, [status(thm)], [c120,c87])). % 44.42/6.60 cnf(d108, plain, op(e1,e0) != e1, inference(resolution, [status(thm)], [d86,d107])). % 44.42/6.60 cnf(d109, plain, $false, inference(resolution, [status(thm)], [d108,d106])). % 44.42/6.60 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------