%------------------------------------------------------------------------------
% File : MaedMax---1.4
% Problem : PUZ054-10 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp
% Command : run_maedmax %d %s
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Jul 26 07:11:20 EDT 2022
% Result : Satisfiable 65.57s 65.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : PUZ054-10 : TPTP v8.1.0. Released v7.5.0.
% 0.03/0.12 % Command : run_maedmax %d %s
% 0.11/0.33 % Computer : n027.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Tue Jul 26 02:46:35 EDT 2022
% 0.11/0.33 % CPUTime :
% 65.57/65.79 % SZS status Satisfiable
% 65.57/65.79 % SZS output start Saturation for /tmp/MaedMax_12544
% 65.57/65.79 cnf(eq_0, axiom, (A = ifeq(B,B,A,C)), file('/tmp/MaedMax_12544')).
% 65.57/65.79 cnf(eq_1, axiom,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = true),
% 65.57/65.79 file('/tmp/MaedMax_12544')).
% 65.57/65.79 cnf(eq_2, axiom, (ifeq(p(s(s(A)),B),true,p(A,s(B)),true) = true),
% 65.57/65.79 file('/tmp/MaedMax_12544')).
% 65.57/65.79 cnf(eq_3, axiom, (ifeq(p(A,s(s(B))),true,p(A,s(B)),true) = true),
% 65.57/65.79 file('/tmp/MaedMax_12544')).
% 65.57/65.79 cnf(eq_4, axiom, (ifeq(p(s(A),s(B)),true,p(s(A),B),true) = true),
% 65.57/65.79 file('/tmp/MaedMax_12544')).
% 65.57/65.79 cnf(eq_5, plain,
% 65.57/65.79 (ifeq(true,true,p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(n0))))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_1, eq_3])).
% 65.57/65.79 cnf(eq_6, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_1, eq_3])).
% 65.57/65.79 cnf(eq_7, plain,
% 65.57/65.79 (ifeq(true,true,p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_1, eq_2])).
% 65.57/65.79 cnf(eq_8, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(s(s(s(n0))))))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_1, eq_2])).
% 65.57/65.79 cnf(eq_9, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_7, eq_0])).
% 65.57/65.79 cnf(eq_10, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(n0))))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_5, eq_0])).
% 65.57/65.79 cnf(eq_11, plain,
% 65.57/65.79 (ifeq(p(x100,s(s(x101))),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0)))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_1, eq_3])).
% 65.57/65.79 cnf(eq_12, plain,
% 65.57/65.79 (ifeq(p(x100,s(s(x101))),true,p(x100,s(x101)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0))))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_1, eq_3])).
% 65.57/65.79 cnf(eq_13, plain,
% 65.57/65.79 (ifeq(p(s(x100),s(x101)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0)))))))))),p(s(x100),x101),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_1, eq_4])).
% 65.57/65.79 cnf(eq_14, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0)))))))))),p(s(A),B),true) = true),
% 65.57/65.79 eq_13).
% 65.57/65.79 cnf(eq_15, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0)))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_11).
% 65.57/65.79 cnf(eq_16, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),true,p(A,s(B)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0))))))))))) = true),
% 65.57/65.79 eq_12).
% 65.57/65.79 cnf(eq_17, plain,
% 65.57/65.79 (ifeq(p(x100,s(s(x101))),p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_9, eq_3])).
% 65.57/65.79 cnf(eq_18, plain,
% 65.57/65.79 (ifeq(p(s(x100),s(x101)),p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),p(s(x100),x101),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_9, eq_4])).
% 65.57/65.79 cnf(eq_19, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_9, eq_2])).
% 65.57/65.79 cnf(eq_20, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),p(s(A),B),true) = true),
% 65.57/65.79 eq_18).
% 65.57/65.79 cnf(eq_21, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_19).
% 65.57/65.79 cnf(eq_22, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_17).
% 65.57/65.79 cnf(eq_23, plain,
% 65.57/65.79 (ifeq(p(x100,s(s(x101))),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(n0))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_10, eq_3])).
% 65.57/65.79 cnf(eq_24, plain,
% 65.57/65.79 (ifeq(p(s(x100),s(x101)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(n0))))))))),p(s(x100),x101),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_10, eq_4])).
% 65.57/65.79 cnf(eq_25, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(n0))))))))),p(s(A),B),true) = true),
% 65.57/65.79 eq_24).
% 65.57/65.79 cnf(eq_26, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(n0))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_23).
% 65.57/65.79 cnf(eq_27, plain,
% 65.57/65.79 (true = p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_21, eq_0])).
% 65.57/65.79 cnf(eq_28, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_22])).
% 65.57/65.79 cnf(eq_29, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_21])).
% 65.57/65.79 cnf(eq_30, plain,
% 65.57/65.79 (true = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_25, eq_0])).
% 65.57/65.79 cnf(eq_31, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0)))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_26])).
% 65.57/65.79 cnf(eq_32, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_9, eq_3])).
% 65.57/65.79 cnf(eq_33, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(s(s(n0)))))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_10, eq_2])).
% 65.57/65.79 cnf(eq_34, plain,
% 65.57/65.79 (ifeq(p(x100,s(s(x101))),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0)))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_30, eq_3])).
% 65.57/65.79 cnf(eq_35, plain,
% 65.57/65.79 (ifeq(p(x100,s(s(x101))),true,p(x100,s(x101)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_30, eq_3])).
% 65.57/65.79 cnf(eq_36, plain,
% 65.57/65.79 (ifeq(p(s(x100),s(x101)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0)))))))),p(s(x100),x101),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_30, eq_4])).
% 65.57/65.79 cnf(eq_37, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0)))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_30, eq_2])).
% 65.57/65.79 cnf(eq_38, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0)))))))),p(s(A),B),true) = true),
% 65.57/65.79 eq_36).
% 65.57/65.79 cnf(eq_39, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0)))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_37).
% 65.57/65.79 cnf(eq_40, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0)))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_34).
% 65.57/65.79 cnf(eq_41, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),true,p(A,s(B)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0))))))))) = true),
% 65.57/65.79 eq_35).
% 65.57/65.79 cnf(eq_42, plain,
% 65.57/65.79 (ifeq(p(x100,s(s(x101))),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_27, eq_3])).
% 65.57/65.79 cnf(eq_43, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_27, eq_2])).
% 65.57/65.79 cnf(eq_44, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_43).
% 65.57/65.79 cnf(eq_45, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_42).
% 65.57/65.79 cnf(eq_46, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_45])).
% 65.57/65.79 cnf(eq_47, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_44])).
% 65.57/65.79 cnf(eq_48, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(n0))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_40])).
% 65.57/65.79 cnf(eq_49, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(n0))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_39])).
% 65.57/65.79 cnf(eq_50, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(n0))))))))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_49, eq_9])).
% 65.57/65.79 cnf(eq_51, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_47, eq_9])).
% 65.57/65.79 cnf(eq_52, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_48, eq_9])).
% 65.57/65.79 cnf(eq_53, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_46, eq_9])).
% 65.57/65.79 cnf(eq_54, plain,
% 65.57/65.79 (ifeq(p(s(x100),s(x101)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(n0))))))),p(s(x100),x101),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_52, eq_20])).
% 65.57/65.79 cnf(eq_55, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(n0))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_52, eq_21])).
% 65.57/65.79 cnf(eq_56, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(n0))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_50, eq_21])).
% 65.57/65.79 cnf(eq_57, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_53, eq_21])).
% 65.57/65.79 cnf(eq_58, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_51, eq_21])).
% 65.57/65.79 cnf(eq_59, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(n0))))))),p(s(A),B),true) = true),
% 65.57/65.79 eq_54).
% 65.57/65.79 cnf(eq_60, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(n0))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_55).
% 65.57/65.79 cnf(eq_61, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(n0))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_56).
% 65.57/65.79 cnf(eq_62, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_57).
% 65.57/65.79 cnf(eq_63, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_58).
% 65.57/65.79 cnf(eq_64, plain,
% 65.57/65.79 (true = p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_61, eq_0])).
% 65.57/65.79 cnf(eq_65, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_61])).
% 65.57/65.79 cnf(eq_66, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(n0)))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_60])).
% 65.57/65.79 cnf(eq_67, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_64, eq_10])).
% 65.57/65.79 cnf(eq_68, plain,
% 65.57/65.79 (true = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_62, eq_0])).
% 65.57/65.79 cnf(eq_69, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_62])).
% 65.57/65.79 cnf(eq_70, plain,
% 65.57/65.79 (true = p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_63, eq_0])).
% 65.57/65.79 cnf(eq_71, plain,
% 65.57/65.79 (true = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(n0))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_59, eq_0])).
% 65.57/65.79 cnf(eq_72, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(n0)))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_59])).
% 65.57/65.79 cnf(eq_73, plain,
% 65.57/65.79 (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_63])).
% 65.57/65.79 cnf(eq_74, plain,
% 65.57/65.79 (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_70, eq_30])).
% 65.57/65.79 cnf(eq_75, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(n0)))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_71, eq_30])).
% 65.57/65.79 cnf(eq_76, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_64, eq_30])).
% 65.57/65.79 cnf(eq_77, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_68, eq_30])).
% 65.57/65.79 cnf(eq_78, plain,
% 65.57/65.79 (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) = p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_74, eq_76])).
% 65.57/65.79 cnf(eq_79, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_77, eq_76])).
% 65.57/65.79 cnf(eq_80, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(n0))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_75, eq_76])).
% 65.57/65.79 cnf(eq_81, plain,
% 65.57/65.79 (ifeq(p(x100,s(s(x101))),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_76, eq_40])).
% 65.57/65.79 cnf(eq_82, plain,
% 65.57/65.79 (ifeq(p(x100,s(s(x101))),true,p(x100,s(x101)),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0))))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_76, eq_41])).
% 65.57/65.79 cnf(eq_83, plain,
% 65.57/65.79 (ifeq(p(s(x100),s(x101)),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))),p(s(x100),x101),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_76, eq_38])).
% 65.57/65.79 cnf(eq_84, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_76, eq_39])).
% 65.57/65.79 cnf(eq_85, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))),p(s(A),B),true) = true),
% 65.57/65.79 eq_83).
% 65.57/65.79 cnf(eq_86, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_81).
% 65.57/65.79 cnf(eq_87, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),true,p(A,s(B)),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0))))))))))) = true),
% 65.57/65.79 eq_82).
% 65.57/65.79 cnf(eq_88, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_84).
% 65.57/65.79 cnf(eq_89, plain,
% 65.57/65.79 (true = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_88, eq_0])).
% 65.57/65.79 cnf(eq_90, plain,
% 65.57/65.79 (true = p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_85, eq_0])).
% 65.57/65.79 cnf(eq_91, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_86])).
% 65.57/65.79 cnf(eq_92, plain,
% 65.57/65.79 (ifeq(p(s(x100),s(x101)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(n0)))))),p(s(x100),x101),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_80, eq_85])).
% 65.57/65.79 cnf(eq_93, plain,
% 65.57/65.79 (ifeq(p(s(x100),s(x101)),p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),p(s(x100),x101),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_79, eq_85])).
% 65.57/65.79 cnf(eq_94, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_88])).
% 65.57/65.79 cnf(eq_95, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(n0)))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_80, eq_88])).
% 65.57/65.79 cnf(eq_96, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_79, eq_88])).
% 65.57/65.79 cnf(eq_97, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_78, eq_88])).
% 65.57/65.79 cnf(eq_98, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(n0)))))),p(s(A),B),true) = true),
% 65.57/65.79 eq_92).
% 65.57/65.79 cnf(eq_99, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),p(s(A),B),true) = true),
% 65.57/65.79 eq_93).
% 65.57/65.79 cnf(eq_100, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(n0)))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_95).
% 65.57/65.79 cnf(eq_101, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_96).
% 65.57/65.79 cnf(eq_102, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_97).
% 65.57/65.79 cnf(eq_103, plain,
% 65.57/65.79 (true = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_100, eq_0])).
% 65.57/65.79 cnf(eq_104, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_100])).
% 65.57/65.79 cnf(eq_105, plain,
% 65.57/65.79 (true = p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_101, eq_0])).
% 65.57/65.79 cnf(eq_106, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_102])).
% 65.57/65.79 cnf(eq_107, plain,
% 65.57/65.79 (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_101])).
% 65.57/65.79 cnf(eq_108, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(s(n0))))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_31, eq_2])).
% 65.57/65.79 cnf(eq_109, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_29, eq_3])).
% 65.57/65.79 cnf(eq_110, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(n0)))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_48, eq_2])).
% 65.57/65.79 cnf(eq_111, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_47, eq_68])).
% 65.57/65.79 cnf(eq_112, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_111, eq_79])).
% 65.57/65.79 cnf(eq_113, plain,
% 65.57/65.79 (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_105, eq_68])).
% 65.57/65.79 cnf(eq_114, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_89, eq_68])).
% 65.57/65.79 cnf(eq_115, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_103, eq_68])).
% 65.57/65.79 cnf(eq_116, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_90, eq_68])).
% 65.57/65.79 cnf(eq_117, plain,
% 65.57/65.79 (true = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(n0)))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_98, eq_0])).
% 65.57/65.79 cnf(eq_118, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(n0))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_98])).
% 65.57/65.79 cnf(eq_119, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(n0)))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_117, eq_68])).
% 65.57/65.79 cnf(eq_120, plain,
% 65.57/65.79 (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_105, eq_64])).
% 65.57/65.79 cnf(eq_121, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(n0))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_119, eq_101])).
% 65.57/65.79 cnf(eq_122, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0))))))) = p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_115, eq_113])).
% 65.57/65.79 cnf(eq_123, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0))))))))) = p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_116, eq_113])).
% 65.57/65.79 cnf(eq_124, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_114, eq_113])).
% 65.57/65.79 cnf(eq_125, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_114, eq_116])).
% 65.57/65.79 cnf(eq_126, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_114, eq_115])).
% 65.57/65.79 cnf(eq_127, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(n0)))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_114, eq_119])).
% 65.57/65.79 cnf(eq_128, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(n0))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_121).
% 65.57/65.79 cnf(eq_129, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),p(s(A),B),p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) = p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_99, eq_113]), eq_105]),
% 65.57/65.79 eq_105])).
% 65.57/65.79 cnf(eq_130, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),p(A,s(B)),p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) = p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_101, eq_113]), eq_105]),
% 65.57/65.79 eq_105])).
% 65.57/65.79 cnf(eq_131, plain,
% 65.57/65.79 (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_1, eq_105])).
% 65.57/65.79 cnf(eq_132, plain,
% 65.57/65.79 (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_10, eq_105])).
% 65.57/65.79 cnf(eq_133, plain,
% 65.57/65.79 (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_130, eq_0])).
% 65.57/65.79 cnf(eq_134, plain,
% 65.57/65.79 (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_129, eq_0])).
% 65.57/65.79 cnf(eq_135, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_131, eq_133])).
% 65.57/65.79 cnf(eq_136, plain,
% 65.57/65.79 (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_134, eq_132])).
% 65.57/65.79 cnf(eq_137, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_133, eq_131])).
% 65.57/65.79 cnf(eq_138, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_124, eq_133])).
% 65.57/65.79 cnf(eq_139, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_123, eq_133])).
% 65.57/65.79 cnf(eq_140, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_120, eq_133])).
% 65.57/65.79 cnf(eq_141, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_122, eq_133])).
% 65.57/65.79 cnf(eq_142, plain, (true = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_68, eq_113]), eq_133])).
% 65.57/65.79 cnf(eq_143, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_112, eq_140])).
% 65.57/65.79 cnf(eq_144, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_126, eq_138])).
% 65.57/65.79 cnf(eq_145, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_144, eq_137])).
% 65.57/65.79 cnf(eq_146, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_125, eq_139])).
% 65.57/65.79 cnf(eq_147, plain, (p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_47, eq_143])).
% 65.57/65.79 cnf(eq_148, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_15, eq_135])).
% 65.57/65.79 cnf(eq_149, plain, (true = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_148, eq_0])).
% 65.57/65.79 cnf(eq_150, plain,
% 65.57/65.79 (ifeq(p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_147, eq_2])).
% 65.57/65.79 cnf(eq_151, plain, (p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_148])).
% 65.57/65.79 cnf(eq_152, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),true,true,true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_150, eq_133])).
% 65.57/65.79 cnf(eq_153, plain,
% 65.57/65.79 (ifeq(true,true,p(n0,s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_151, eq_3])).
% 65.57/65.79 cnf(eq_154, plain,
% 65.57/65.79 (ifeq(true,true,p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(n0)))))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_94, eq_3])).
% 65.57/65.79 cnf(eq_155, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),p(x100,s(x101)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_149, eq_2])).
% 65.57/65.79 cnf(eq_156, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_146, eq_152])).
% 65.57/65.79 cnf(eq_157, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_89, eq_149])).
% 65.57/65.79 cnf(eq_158, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_149, eq_142])).
% 65.57/65.79 cnf(eq_159, plain, (p(n0,s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_153, eq_0])).
% 65.57/65.79 cnf(eq_160, plain, (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(n0)))))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_154, eq_0])).
% 65.57/65.79 cnf(eq_161, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 eq_155).
% 65.57/65.79 cnf(eq_162, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_94, eq_159])).
% 65.57/65.79 cnf(eq_163, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_47, eq_143]), eq_159])).
% 65.57/65.79 cnf(eq_164, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(n0,s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),p(A,s(B)),p(n0,s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_3, eq_159]), eq_159]),
% 65.57/65.79 eq_159])).
% 65.57/65.79 cnf(eq_165, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_139, eq_163])).
% 65.57/65.79 cnf(eq_166, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_141, eq_163])).
% 65.57/65.79 cnf(eq_167, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_145, eq_166])).
% 65.57/65.79 cnf(eq_168, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_157, eq_156])).
% 65.57/65.79 cnf(eq_169, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_145, eq_167])).
% 65.57/65.79 cnf(eq_170, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_164, eq_0])).
% 65.57/65.79 cnf(eq_171, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),true,p(n0,s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_159, eq_168])).
% 65.57/65.79 cnf(eq_172, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),true,p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_170, eq_171])).
% 65.57/65.79 cnf(eq_173, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_169, eq_170])).
% 65.57/65.79 cnf(eq_174, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_163, eq_170])).
% 65.57/65.79 cnf(eq_175, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_162, eq_170])).
% 65.57/65.79 cnf(eq_176, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_165, eq_170])).
% 65.57/65.79 cnf(eq_177, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_140, eq_163]), eq_170])).
% 65.57/65.79 cnf(eq_178, plain, (true = p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_159, eq_170])).
% 65.57/65.79 cnf(eq_179, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_67, eq_177])).
% 65.57/65.79 cnf(eq_180, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_145, eq_173])).
% 65.57/65.79 cnf(eq_181, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_158, eq_174])).
% 65.57/65.79 cnf(eq_182, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_125, eq_175])).
% 65.57/65.79 cnf(eq_183, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_160, eq_178])).
% 65.57/65.79 cnf(eq_184, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(n0)))))))))) = p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_183, eq_182])).
% 65.57/65.79 cnf(eq_185, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_125, eq_176])).
% 65.57/65.79 cnf(eq_186, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))),p(A,s(B)),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_87, eq_178]), eq_178])).
% 65.57/65.79 cnf(eq_187, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_186, eq_0])).
% 65.57/65.79 cnf(eq_188, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_185, eq_187])).
% 65.57/65.79 cnf(eq_189, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_170, eq_187])).
% 65.57/65.79 cnf(eq_190, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_181, eq_187])).
% 65.57/65.79 cnf(eq_191, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))) = p(n0,s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_163, eq_170]), eq_187])).
% 65.57/65.79 cnf(eq_192, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(n0))))))))) = p(n0,s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_179, eq_187])).
% 65.57/65.79 cnf(eq_193, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = p(n0,s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_180, eq_187])).
% 65.57/65.79 cnf(eq_194, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(n0)))))))))) = p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_136, eq_192])).
% 65.57/65.79 cnf(eq_195, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(n0,s(s(s(s(s(s(s(s(s(n0)))))))))),p(s(A),B),true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_14, eq_193])).
% 65.57/65.79 cnf(eq_196, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(n0,s(s(s(s(s(s(s(s(s(n0)))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_161, eq_190])).
% 65.57/65.79 cnf(eq_197, plain, (p(n0,s(s(s(s(s(s(s(s(s(n0)))))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_159, eq_189])).
% 65.57/65.79 cnf(eq_198, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(n0,s(s(s(s(s(s(s(s(s(n0)))))))))),p(A,s(B)),true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_15, eq_193])).
% 65.57/65.79 cnf(eq_199, plain, (true = p(n0,s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_198, eq_0])).
% 65.57/65.79 cnf(eq_200, plain, (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0)))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_128])).
% 65.57/65.79 cnf(eq_201, plain, (p(n0,s(s(s(s(s(s(s(s(n0))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_198])).
% 65.57/65.79 cnf(eq_202, plain, (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_194, eq_197])).
% 65.57/65.79 cnf(eq_203, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(n0))))))))) = p(n0,s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_201, eq_197])).
% 65.57/65.79 cnf(eq_204, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_188, eq_203])).
% 65.57/65.79 cnf(eq_205, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(n0))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_125, eq_204]), eq_176])).
% 65.57/65.79 cnf(eq_206, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(n0))))))))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_200, eq_199])).
% 65.57/65.79 cnf(eq_207, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(n0,s(s(s(s(s(s(s(s(n0))))))))),p(A,s(B)),p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(n0,s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_16, eq_199]), eq_180]),
% 65.57/65.79 eq_199])).
% 65.57/65.79 cnf(eq_208, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(n0))))))))) = p(n0,s(s(s(s(s(s(s(n0))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_207, eq_0])).
% 65.57/65.79 cnf(eq_209, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0))))))))) = p(n0,s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_176, eq_187]), eq_203])).
% 65.57/65.79 cnf(eq_210, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(n0))))))))) = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_184, eq_209])).
% 65.57/65.79 cnf(eq_211, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0)))))) = p(n0,s(s(s(s(s(s(s(n0))))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_206, eq_208])).
% 65.57/65.79 cnf(eq_212, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(n0)))))))))) = p(n0,s(s(s(s(s(s(s(n0))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_203, eq_208])).
% 65.57/65.79 cnf(eq_213, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = p(n0,s(s(s(s(s(s(s(n0))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_180, eq_205]), eq_208])).
% 65.57/65.79 cnf(eq_214, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(n0)))))))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_145, eq_213])).
% 65.57/65.79 cnf(eq_215, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(n0,s(s(s(s(s(s(s(n0)))))))),p(s(A),B),true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_195, eq_212])).
% 65.57/65.79 cnf(eq_216, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(n0,s(s(s(s(s(s(s(n0)))))))),p(A,s(B)),true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_196, eq_212])).
% 65.57/65.79 cnf(eq_217, plain, (p(n0,s(s(s(s(s(s(s(n0)))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_197, eq_212])).
% 65.57/65.79 cnf(eq_218, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(n0,s(s(s(s(s(s(s(n0)))))))),p(A,s(B)),true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_198, eq_212])).
% 65.57/65.79 cnf(eq_219, plain, (true = p(n0,s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_218, eq_0])).
% 65.57/65.79 cnf(eq_220, plain, (p(n0,s(s(s(s(s(s(n0))))))) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_218])).
% 65.57/65.79 cnf(eq_221, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(s(n0)))))))),p(n0,s(s(s(s(s(s(s(n0)))))))),p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(n0))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_211, eq_218])).
% 65.57/65.79 cnf(eq_222, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(s(s(n0))))))))),p(n0,s(s(s(s(s(s(s(n0)))))))),p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(n0))))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_210, eq_218])).
% 65.57/65.79 cnf(eq_223, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(s(n0)))))))),p(n0,s(s(s(s(s(s(s(n0)))))))),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0)))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_214, eq_216])).
% 65.57/65.79 cnf(eq_224, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(s(n0)))))))),p(n0,s(s(s(s(s(s(s(n0)))))))),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(n0))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_211, eq_216])).
% 65.57/65.79 cnf(eq_225, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(s(s(n0))))))))),p(n0,s(s(s(s(s(s(s(n0)))))))),p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(n0))))))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_210, eq_216])).
% 65.57/65.79 cnf(eq_226, plain, (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0)))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_223, eq_0])).
% 65.57/65.79 cnf(eq_227, plain, (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(n0))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_224, eq_0])).
% 65.57/65.79 cnf(eq_228, plain, (p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_225, eq_208]), eq_0])).
% 65.57/65.79 cnf(eq_229, plain, (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(n0))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_221, eq_0])).
% 65.57/65.79 cnf(eq_230, plain, (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(n0))))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_222, eq_208]), eq_0])).
% 65.57/65.79 cnf(eq_231, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(n0))))))) = p(n0,s(s(s(s(s(s(s(n0))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_220, eq_217])).
% 65.57/65.79 cnf(eq_232, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(n0)))))))))) = p(n0,s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_212, eq_231])).
% 65.57/65.79 cnf(eq_233, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_205, eq_208]), eq_231])).
% 65.57/65.79 cnf(eq_234, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_188, eq_212]), eq_231])).
% 65.57/65.79 cnf(eq_235, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(n0))))))) = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_230, eq_219])).
% 65.57/65.79 cnf(eq_236, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(n0))))))) = p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_227, eq_219])).
% 65.57/65.79 cnf(eq_237, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(n0))))))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(n0)))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_229, eq_219])).
% 65.57/65.79 cnf(eq_238, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(n0,s(s(s(s(s(s(n0))))))),p(A,s(B)),p(n0,s(s(s(s(s(s(n0)))))))) = p(n0,s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_198, eq_232]), eq_219]),
% 65.57/65.79 eq_219])).
% 65.57/65.79 cnf(eq_239, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(n0)))))))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_158, eq_191])).
% 65.57/65.79 cnf(eq_240, plain, (p(n0,s(s(s(s(s(s(n0))))))) = p(n0,s(s(s(s(s(n0))))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_238, eq_0])).
% 65.57/65.79 cnf(eq_241, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(n0)))))))))) = p(n0,s(s(s(s(s(n0))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_232, eq_240])).
% 65.57/65.79 cnf(eq_242, plain,
% 65.57/65.79 (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(s(s(n0))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_234, eq_240])).
% 65.57/65.79 cnf(eq_243, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(n0)))))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(n0)))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_127, eq_242])).
% 65.57/65.79 cnf(eq_244, plain, (p(n0,s(s(s(s(s(n0)))))) = p(n0,s(s(s(s(s(s(s(n0))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_220, eq_240]), eq_217])).
% 65.57/65.79 cnf(eq_245, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(n0)))))) = p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_239, eq_241])).
% 65.57/65.79 cnf(eq_246, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(n0,s(s(s(s(s(n0)))))),p(s(A),B),true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_215, eq_244])).
% 65.57/65.79 cnf(eq_247, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(n0,s(s(s(s(s(n0)))))),p(A,s(B)),true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_216, eq_244])).
% 65.57/65.79 cnf(eq_248, plain, (p(n0,s(s(s(s(s(n0)))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_217, eq_244])).
% 65.57/65.79 cnf(eq_249, plain, (ifeq(true,true,p(n0,s(s(s(s(n0))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_248, eq_3])).
% 65.57/65.79 cnf(eq_250, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(n0)))))),p(n0,s(s(s(s(s(n0)))))),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(n0)))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_243, eq_246])).
% 65.57/65.79 cnf(eq_251, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(n0))))))),p(n0,s(s(s(s(s(n0)))))),p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(n0)))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_237, eq_246])).
% 65.57/65.79 cnf(eq_252, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(n0))))))),p(n0,s(s(s(s(s(n0)))))),p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(n0)))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_236, eq_246])).
% 65.57/65.79 cnf(eq_253, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(n0))))))),p(n0,s(s(s(s(s(n0)))))),p(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0)))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_235, eq_246])).
% 65.57/65.79 cnf(eq_254, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(n0))))))),p(n0,s(s(s(s(s(n0)))))),p(s(s(n0)),s(s(s(s(s(s(s(s(s(n0)))))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_235, eq_247])).
% 65.57/65.79 cnf(eq_255, plain, (p(s(s(n0)),s(s(s(s(s(s(s(s(s(n0)))))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_254, eq_240]), eq_0])).
% 65.57/65.79 cnf(eq_256, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(n0)))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_250, eq_0])).
% 65.57/65.79 cnf(eq_257, plain, (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(n0)))) = true),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_251, eq_240]), eq_0])).
% 65.57/65.79 cnf(eq_258, plain, (p(s(s(s(s(s(s(n0)))))),s(s(s(s(s(n0)))))) = true),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_252, eq_240]), eq_0])).
% 65.57/65.79 cnf(eq_259, plain, (p(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0)))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_253, eq_240]), eq_0])).
% 65.57/65.79 cnf(eq_260, plain, (p(n0,s(s(s(s(n0))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_249, eq_0])).
% 65.57/65.79 cnf(eq_261, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(n0,s(s(s(s(n0))))),p(A,s(B)),p(n0,s(s(s(s(n0)))))) = p(n0,s(s(s(s(n0)))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_2, eq_260]), eq_260]),
% 65.57/65.79 eq_260])).
% 65.57/65.79 cnf(eq_262, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(n0,s(s(s(s(n0))))),p(s(A),B),p(n0,s(s(s(s(n0)))))) = p(n0,s(s(s(s(n0)))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_4, eq_260]), eq_260]),
% 65.57/65.79 eq_260])).
% 65.57/65.79 cnf(eq_263, plain, (p(n0,s(s(s(s(n0))))) = p(n0,s(s(s(s(s(n0))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_248, eq_260])).
% 65.57/65.79 cnf(eq_264, plain,
% 65.57/65.79 (p(n0,s(s(s(s(n0))))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(n0))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_257, eq_260])).
% 65.57/65.79 cnf(eq_265, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(n0,s(s(s(s(n0))))),p(A,s(B)),p(n0,s(s(s(s(n0)))))) = p(n0,s(s(s(s(n0)))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_3, eq_260]), eq_260]),
% 65.57/65.79 eq_260])).
% 65.57/65.79 cnf(eq_266, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(s(n0)))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_233, eq_240]), eq_263])).
% 65.57/65.79 cnf(eq_267, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))) = p(n0,s(s(s(s(n0)))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_245, eq_263])).
% 65.57/65.79 cnf(eq_268, plain,
% 65.57/65.79 (p(n0,s(s(s(s(n0))))) = p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_172, eq_267]), eq_260]),
% 65.57/65.79 eq_260]),
% 65.57/65.79 eq_0]),
% 65.57/65.79 eq_260])).
% 65.57/65.79 cnf(eq_269, plain, (p(n0,s(s(s(s(n0))))) = p(n0,s(s(s(n0))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_265, eq_0])).
% 65.57/65.79 cnf(eq_270, plain,
% 65.57/65.79 (ifeq(p(s(x100),s(x101)),p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))),p(s(x100),x101),p(n0,s(s(s(s(n0)))))) = p(n0,s(s(s(s(n0)))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_268, eq_262])).
% 65.57/65.79 cnf(eq_271, plain,
% 65.57/65.79 (ifeq(p(s(s(x100)),x101),p(n0,s(s(s(s(n0))))),p(x100,s(x101)),p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(n0,s(s(s(s(n0)))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_268, eq_261])).
% 65.57/65.79 cnf(eq_272, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(n0,s(s(s(s(n0))))),p(A,s(B)),p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))) = p(n0,s(s(s(s(n0)))))),
% 65.57/65.79 eq_271).
% 65.57/65.79 cnf(eq_273, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))),p(s(A),B),p(n0,s(s(s(s(n0)))))) = p(n0,s(s(s(s(n0)))))),
% 65.57/65.79 eq_270).
% 65.57/65.79 cnf(eq_274, plain, (p(n0,s(s(s(s(s(s(n0))))))) = p(n0,s(s(s(n0))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_240, eq_263]), eq_269])).
% 65.57/65.79 cnf(eq_275, plain,
% 65.57/65.79 (p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))) = p(n0,s(s(s(n0))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_266, eq_269])).
% 65.57/65.79 cnf(eq_276, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(n0)))) = p(n0,s(s(s(n0))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_264, eq_269])).
% 65.57/65.79 cnf(eq_277, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(n0,s(s(s(n0)))),p(s(A),B),p(n0,s(s(s(n0))))) = p(n0,s(s(s(n0))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_273, eq_275]), eq_269]),
% 65.57/65.79 eq_269])).
% 65.57/65.79 cnf(eq_278, plain, (p(n0,s(s(s(n0)))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_260, eq_269])).
% 65.57/65.79 cnf(eq_279, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(n0,s(s(s(n0)))),p(A,s(B)),p(n0,s(s(s(n0))))) = p(n0,s(s(s(n0))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_272, eq_269]), eq_275]),
% 65.57/65.79 eq_269])).
% 65.57/65.79 cnf(eq_280, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(n0)))),p(n0,s(s(s(n0)))),p(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0))),p(n0,s(s(s(n0))))) = p(n0,s(s(s(n0))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_276, eq_277])).
% 65.57/65.79 cnf(eq_281, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(n0)))),p(n0,s(s(s(n0)))),p(s(s(s(s(s(s(n0)))))),s(s(s(s(n0))))),p(n0,s(s(s(n0))))) = p(n0,s(s(s(n0))))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_276, eq_279])).
% 65.57/65.79 cnf(eq_282, plain,
% 65.57/65.79 (p(n0,s(s(s(n0)))) = p(s(s(s(s(s(s(n0)))))),s(s(s(s(n0)))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_281, eq_0])).
% 65.57/65.79 cnf(eq_283, plain,
% 65.57/65.79 (p(n0,s(s(s(n0)))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_280, eq_0])).
% 65.57/65.79 cnf(eq_284, plain, (ifeq(true,true,p(n0,s(s(n0))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_278, eq_3])).
% 65.57/65.79 cnf(eq_285, plain,
% 65.57/65.79 (ifeq(true,true,p(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_257, eq_3])).
% 65.57/65.79 cnf(eq_286, plain,
% 65.57/65.79 (ifeq(true,true,p(s(s(s(s(s(s(n0)))))),s(s(s(s(n0))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_257, eq_2])).
% 65.57/65.79 cnf(eq_287, plain, (p(s(s(s(s(s(s(n0)))))),s(s(s(s(n0))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_286, eq_0])).
% 65.57/65.79 cnf(eq_288, plain, (p(n0,s(s(n0))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_284, eq_0])).
% 65.57/65.79 cnf(eq_289, plain, (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_285, eq_0])).
% 65.57/65.79 cnf(eq_290, plain,
% 65.57/65.79 (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_257, eq_288])).
% 65.57/65.79 cnf(eq_291, plain, (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_289, eq_288])).
% 65.57/65.79 cnf(eq_292, plain, (p(s(s(s(s(s(s(n0)))))),s(s(s(s(n0))))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_287, eq_288])).
% 65.57/65.79 cnf(eq_293, plain, (p(n0,s(s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_278, eq_288])).
% 65.57/65.79 cnf(eq_294, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(n0,s(s(n0))),p(A,s(B)),p(n0,s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_3, eq_288]), eq_288]),
% 65.57/65.79 eq_288])).
% 65.57/65.79 cnf(eq_295, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(n0,s(s(n0))),p(A,s(B)),p(n0,s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_2, eq_288]), eq_288]),
% 65.57/65.79 eq_288])).
% 65.57/65.79 cnf(eq_296, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(n0,s(s(n0))),p(s(A),B),p(n0,s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_4, eq_288]), eq_288]),
% 65.57/65.79 eq_288])).
% 65.57/65.79 cnf(eq_297, plain, (p(n0,s(s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_294, eq_0])).
% 65.57/65.79 cnf(eq_298, plain, (p(n0,s(n0)) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_0, eq_294])).
% 65.57/65.79 cnf(eq_299, plain,
% 65.57/65.79 (ifeq(true,p(n0,s(s(n0))),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(n0))))))),p(n0,s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_31, eq_294])).
% 65.57/65.79 cnf(eq_300, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(n0)))),p(n0,s(s(n0))),p(s(s(s(s(s(s(s(s(n0)))))))),s(n0)),p(n0,s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_283, eq_294])).
% 65.57/65.79 cnf(eq_301, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(n0)))),p(n0,s(s(n0))),p(s(s(s(s(s(s(n0)))))),s(s(s(n0)))),p(n0,s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_282, eq_294])).
% 65.57/65.79 cnf(eq_302, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(n0)))),p(n0,s(s(n0))),p(s(s(s(s(n0)))),s(s(s(s(s(n0)))))),p(n0,s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_282, eq_295])).
% 65.57/65.79 cnf(eq_303, plain, (p(n0,s(s(n0))) = p(s(s(s(s(n0)))),s(s(s(s(s(n0))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_302, eq_293]), eq_0])).
% 65.57/65.79 cnf(eq_304, plain, (p(n0,s(s(n0))) = p(s(s(s(s(s(s(s(s(n0)))))))),s(n0))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_300, eq_293]), eq_0])).
% 65.57/65.79 cnf(eq_305, plain, (p(n0,s(s(n0))) = p(s(s(s(s(s(s(n0)))))),s(s(s(n0))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_301, eq_293]), eq_0])).
% 65.57/65.79 cnf(eq_306, plain,
% 65.57/65.79 (p(n0,s(s(n0))) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_299, eq_288]), eq_0])).
% 65.57/65.79 cnf(eq_307, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(n0))),p(n0,s(s(n0))),p(s(s(s(s(s(s(n0)))))),s(s(n0))),p(n0,s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_305, eq_294])).
% 65.57/65.79 cnf(eq_308, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(n0))),p(n0,s(s(n0))),p(s(s(s(s(n0)))),s(s(s(s(n0))))),p(n0,s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_303, eq_294])).
% 65.57/65.79 cnf(eq_309, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(n0))),p(n0,s(s(n0))),p(s(s(s(s(s(s(s(s(n0)))))))),n0),p(n0,s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_304, eq_296])).
% 65.57/65.79 cnf(eq_310, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(n0))),p(n0,s(s(n0))),p(s(s(n0)),s(s(s(s(s(s(n0))))))),p(n0,s(s(n0)))) = p(n0,s(s(n0)))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_303, eq_295])).
% 65.57/65.79 cnf(eq_311, plain, (p(s(s(s(s(s(s(s(s(n0)))))))),s(n0)) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_304, eq_297])).
% 65.57/65.79 cnf(eq_312, plain, (p(s(s(s(s(s(s(n0)))))),s(s(s(n0)))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_305, eq_297])).
% 65.57/65.79 cnf(eq_313, plain, (p(s(s(s(s(n0)))),s(s(s(s(s(n0)))))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_303, eq_297])).
% 65.57/65.79 cnf(eq_314, plain, (p(n0,s(s(n0))) = p(s(s(n0)),s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_310, eq_0])).
% 65.57/65.79 cnf(eq_315, plain, (p(n0,s(s(n0))) = p(s(s(s(s(s(s(s(s(n0)))))))),n0)),
% 65.57/65.79 inference(rw, [status(thm)], [eq_309, eq_0])).
% 65.57/65.79 cnf(eq_316, plain, (p(n0,s(s(n0))) = p(s(s(s(s(s(s(n0)))))),s(s(n0)))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_307, eq_0])).
% 65.57/65.79 cnf(eq_317, plain, (p(n0,s(s(n0))) = p(s(s(s(s(n0)))),s(s(s(s(n0)))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_308, eq_0])).
% 65.57/65.79 cnf(eq_318, plain, (p(n0,s(s(s(s(s(s(n0))))))) = p(n0,s(n0))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_274, eq_293]), eq_297])).
% 65.57/65.79 cnf(eq_319, plain, (p(s(s(s(s(s(s(n0)))))),s(s(s(s(n0))))) = p(n0,s(n0))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_292, eq_297])).
% 65.57/65.79 cnf(eq_320, plain, (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_291, eq_297])).
% 65.57/65.79 cnf(eq_321, plain, (p(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(n0)))) = p(n0,s(n0))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_290, eq_297])).
% 65.57/65.79 cnf(eq_322, plain, (true = p(n0,s(n0))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_288, eq_297])).
% 65.57/65.79 cnf(eq_323, plain,
% 65.57/65.79 (ifeq(p(A,s(s(B))),p(n0,s(n0)),p(A,s(B)),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_3, eq_322]), eq_322]),
% 65.57/65.79 eq_322])).
% 65.57/65.79 cnf(eq_324, plain,
% 65.57/65.79 (ifeq(p(s(s(A)),B),p(n0,s(n0)),p(A,s(B)),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_2, eq_322]), eq_322]),
% 65.57/65.79 eq_322])).
% 65.57/65.79 cnf(eq_325, plain,
% 65.57/65.79 (ifeq(p(s(A),s(B)),p(n0,s(n0)),p(s(A),B),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_4, eq_322]), eq_322]),
% 65.57/65.79 eq_322])).
% 65.57/65.79 cnf(eq_326, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(n0))),p(n0,s(n0)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(n0)))))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_306, eq_323])).
% 65.57/65.79 cnf(eq_327, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(n0))),p(n0,s(n0)),p(s(s(s(s(s(s(n0)))))),s(n0)),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_316, eq_323])).
% 65.57/65.79 cnf(eq_328, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(n0))),p(n0,s(n0)),p(s(s(s(s(n0)))),s(s(s(n0)))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_317, eq_323])).
% 65.57/65.79 cnf(eq_329, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(n0))),p(n0,s(n0)),p(s(s(n0)),s(s(s(s(s(n0)))))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_314, eq_323])).
% 65.57/65.79 cnf(eq_330, plain,
% 65.57/65.79 (p(n0,s(n0)) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(n0))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_326, eq_297]), eq_0])).
% 65.57/65.79 cnf(eq_331, plain, (p(n0,s(n0)) = p(s(s(s(s(s(s(n0)))))),s(n0))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_327, eq_297]), eq_0])).
% 65.57/65.79 cnf(eq_332, plain, (p(n0,s(n0)) = p(s(s(s(s(n0)))),s(s(s(n0))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_328, eq_297]), eq_0])).
% 65.57/65.79 cnf(eq_333, plain, (p(n0,s(n0)) = p(s(s(n0)),s(s(s(s(s(n0))))))),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_329, eq_297]), eq_0])).
% 65.57/65.79 cnf(eq_334, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(n0))))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_330, eq_323])).
% 65.57/65.79 cnf(eq_335, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(s(s(n0)))),s(s(n0))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_332, eq_323])).
% 65.57/65.79 cnf(eq_336, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(n0)),s(s(s(s(n0))))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_333, eq_323])).
% 65.57/65.79 cnf(eq_337, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(s(s(s(s(n0)))))),n0),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_331, eq_325])).
% 65.57/65.79 cnf(eq_338, plain, (p(n0,s(n0)) = p(s(s(s(s(s(s(n0)))))),n0)),
% 65.57/65.79 inference(rw, [status(thm)], [eq_337, eq_0])).
% 65.57/65.79 cnf(eq_339, plain,
% 65.57/65.79 (p(n0,s(n0)) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(n0)))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_334, eq_0])).
% 65.57/65.79 cnf(eq_340, plain, (p(n0,s(n0)) = p(s(s(s(s(n0)))),s(s(n0)))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_335, eq_0])).
% 65.57/65.79 cnf(eq_341, plain, (p(n0,s(n0)) = p(s(s(n0)),s(s(s(s(n0)))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_336, eq_0])).
% 65.57/65.79 cnf(eq_342, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(s(s(n0)))),s(n0)),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_340, eq_323])).
% 65.57/65.79 cnf(eq_343, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(n0)),s(s(s(n0)))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_341, eq_323])).
% 65.57/65.79 cnf(eq_344, plain, (p(n0,s(n0)) = p(s(s(s(s(n0)))),s(n0))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_342, eq_0])).
% 65.57/65.79 cnf(eq_345, plain, (p(n0,s(n0)) = p(s(s(n0)),s(s(s(n0))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_343, eq_0])).
% 65.57/65.79 cnf(eq_346, plain, (p(s(s(n0)),s(s(s(s(s(s(n0))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_314, eq_288])).
% 65.57/65.79 cnf(eq_347, plain, (p(s(s(s(s(n0)))),s(s(s(s(n0))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_317, eq_288])).
% 65.57/65.79 cnf(eq_348, plain, (p(s(s(s(s(s(s(n0)))))),s(s(n0))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_316, eq_288])).
% 65.57/65.79 cnf(eq_349, plain, (p(s(s(s(s(s(s(s(s(n0)))))))),n0) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_315, eq_288])).
% 65.57/65.79 cnf(eq_350, plain, (p(n0,s(n0)) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_298, eq_288])).
% 65.57/65.79 cnf(eq_351, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(n0)))),true,p(n0,s(n0)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_339, eq_2])).
% 65.57/65.79 cnf(eq_352, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(n0))))),true,p(n0,s(n0)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_330, eq_2])).
% 65.57/65.79 cnf(eq_353, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(n0)))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_339, eq_323])).
% 65.57/65.79 cnf(eq_354, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(n0)),s(s(n0))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_345, eq_323])).
% 65.57/65.79 cnf(eq_355, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(s(s(n0)))),n0),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_344, eq_325])).
% 65.57/65.79 cnf(eq_356, plain, (p(n0,s(n0)) = p(s(s(s(s(n0)))),n0)),
% 65.57/65.79 inference(rw, [status(thm)], [eq_355, eq_0])).
% 65.57/65.79 cnf(eq_357, plain,
% 65.57/65.79 (p(n0,s(n0)) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(n0))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_353, eq_0])).
% 65.57/65.79 cnf(eq_358, plain, (p(n0,s(n0)) = p(s(s(n0)),s(s(n0)))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_354, eq_0])).
% 65.57/65.79 cnf(eq_359, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(n0))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_357, eq_323])).
% 65.57/65.79 cnf(eq_360, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(n0)),s(n0)),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_358, eq_323])).
% 65.57/65.79 cnf(eq_361, plain,
% 65.57/65.79 (p(n0,s(n0)) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(n0)))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_359, eq_0])).
% 65.57/65.79 cnf(eq_362, plain, (p(n0,s(n0)) = p(s(s(n0)),s(n0))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_360, eq_0])).
% 65.57/65.79 cnf(eq_363, plain, (p(s(s(n0)),s(s(s(s(n0))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_341, eq_350])).
% 65.57/65.79 cnf(eq_364, plain, (p(s(s(n0)),s(s(s(s(s(n0)))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_333, eq_350])).
% 65.57/65.79 cnf(eq_365, plain, (p(s(s(s(s(n0)))),s(s(n0))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_340, eq_350])).
% 65.57/65.79 cnf(eq_366, plain, (p(s(s(s(s(n0)))),s(s(s(n0)))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_332, eq_350])).
% 65.57/65.79 cnf(eq_367, plain, (p(s(s(s(s(s(s(n0)))))),n0) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_338, eq_350])).
% 65.57/65.79 cnf(eq_368, plain, (p(s(s(s(s(s(s(n0)))))),s(n0)) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_331, eq_350])).
% 65.57/65.79 cnf(eq_369, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(n0))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_361, eq_350])).
% 65.57/65.79 cnf(eq_370, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),true,p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(n0)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_361, eq_3])).
% 65.57/65.79 cnf(eq_371, plain, (ifeq(p(n0,s(n0)),true,p(s(s(n0)),n0),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_362, eq_4])).
% 65.57/65.79 cnf(eq_372, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(n0))),true,p(n0,s(n0)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_357, eq_2])).
% 65.57/65.79 cnf(eq_373, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(n0)),true,p(n0,s(n0)),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_361, eq_2])).
% 65.57/65.79 cnf(eq_374, plain, (p(s(s(n0)),n0) = true),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_371, eq_350]), eq_0])).
% 65.57/65.79 cnf(eq_375, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(n0)) = true),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_370, eq_350]), eq_0])).
% 65.57/65.79 cnf(eq_376, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(n0))))),true,true,true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_352, eq_350])).
% 65.57/65.79 cnf(eq_377, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(n0)))),true,true,true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_351, eq_350])).
% 65.57/65.79 cnf(eq_378, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(n0))),true,true,true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_372, eq_350])).
% 65.57/65.79 cnf(eq_379, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(n0)),true,true,true) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_373, eq_350])).
% 65.57/65.79 cnf(eq_380, plain, (p(n0,s(n0)) = p(s(s(n0)),s(s(s(s(s(s(s(s(s(n0))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_255, eq_322])).
% 65.57/65.79 cnf(eq_381, plain, (p(n0,s(n0)) = p(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_259, eq_322])).
% 65.57/65.79 cnf(eq_382, plain, (p(n0,s(n0)) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(n0))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_375, eq_322])).
% 65.57/65.79 cnf(eq_383, plain, (p(n0,s(n0)) = p(s(s(n0)),n0)),
% 65.57/65.79 inference(rw, [status(thm)], [eq_374, eq_322])).
% 65.57/65.79 cnf(eq_384, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(s(s(n0)))),s(s(s(s(s(s(n0))))))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_381, eq_323])).
% 65.57/65.79 cnf(eq_385, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_380, eq_323])).
% 65.57/65.79 cnf(eq_386, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),n0),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_382, eq_325])).
% 65.57/65.79 cnf(eq_387, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),p(n0,s(n0)),p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))),p(n0,s(n0))) = p(n0,s(n0))),
% 65.57/65.79 inference(cp, [status(thm)], [eq_380, eq_324])).
% 65.57/65.79 cnf(eq_388, plain, (p(n0,s(n0)) = p(n0,s(s(s(s(s(s(s(s(s(s(n0)))))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_387, eq_0])).
% 65.57/65.79 cnf(eq_389, plain, (p(n0,s(n0)) = p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),n0)),
% 65.57/65.79 inference(rw, [status(thm)], [eq_386, eq_0])).
% 65.57/65.79 cnf(eq_390, plain, (p(n0,s(n0)) = p(s(s(s(s(n0)))),s(s(s(s(s(s(n0)))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_384, eq_0])).
% 65.57/65.79 cnf(eq_391, plain, (p(n0,s(n0)) = p(s(s(n0)),s(s(s(s(s(s(s(s(n0)))))))))),
% 65.57/65.79 inference(rw, [status(thm)], [eq_385, eq_0])).
% 65.57/65.79 cnf(eq_392, plain, (p(n0,s(s(s(s(s(s(s(s(s(s(n0))))))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_388, eq_350])).
% 65.57/65.79 cnf(eq_393, plain, (p(s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_391, eq_350])).
% 65.57/65.79 cnf(eq_394, plain, (p(s(s(s(s(n0)))),s(s(s(s(s(s(n0))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_390, eq_350])).
% 65.57/65.79 cnf(eq_395, plain, (p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),n0) = true),
% 65.57/65.79 inference(rw, [status(thm)], [eq_389, eq_350])).
% 65.57/65.79 cnf(eq_396, plain,
% 65.57/65.79 (ifeq(p(n0,s(n0)),true,p(s(s(n0)),s(s(s(s(s(s(s(n0)))))))),true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_391, eq_3])).
% 65.57/65.79 cnf(eq_397, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),n0),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_375, eq_2])).
% 65.57/65.79 cnf(eq_398, plain, (p(s(s(n0)),s(s(s(s(s(s(s(n0)))))))) = true),
% 65.57/65.79 inference(rw, [status(thm)],
% 65.57/65.79 [inference(rw, [status(thm)], [eq_396, eq_350]), eq_0])).
% 65.57/65.79 cnf(eq_399, plain,
% 65.57/65.79 (ifeq(p(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_47, eq_3])).
% 65.57/65.79 cnf(eq_400, plain,
% 65.57/65.79 (ifeq(p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_106, eq_3])).
% 65.57/65.79 cnf(eq_401, plain,
% 65.57/65.79 (ifeq(p(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),true,true,true) = true),
% 65.57/65.79 inference(cp, [status(thm)], [eq_73, eq_3])).
% 65.57/65.79 cnf(eq_402, plain, (p(s(s(s(s(s(s(n0)))))),n0) = p(s(s(n0)),s(s(s(s(n0)))))),
% 65.57/65.80 inference(cp, [status(thm)], [eq_367, eq_363])).
% 65.57/65.80
% 65.57/65.80 % SZS output end Saturation
% 65.57/65.80
%------------------------------------------------------------------------------