# Initializing proof state
# Scanning for AC axioms
#
#cnf(i_0_393, plain, (x2_s_1(esk148_0))).
#
#cnf(i_0_399, plain, (x2_s_2(esk153_0))).
#
#cnf(i_0_203, plain, (l_s_13(esk64_0))).
#
#cnf(i_0_412, negated_conjecture, (~l_s_0(X1))).
#
#cnf(i_0_12, plain, (x2_s_5(esk5_0))).
#
#cnf(i_0_100, plain, (l_s_11(esk28_0))).
#
#cnf(i_0_294, plain, (x2_s_3(esk110_0))).
#
#cnf(i_0_97, negated_conjecture, (~x2_s_0(X1))).
#
#cnf(i_0_258, plain, (l_s_3(esk86_0))).
#
#cnf(i_0_210, plain, (a2_s_2(esk67_0))).
#
# Proof found!
# SZS status Theorem

