%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX206-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n008.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 May 5 05:34:43 PM UTC 2026
% Result : Unsatisfiable 0.78s 1.62s
% Output : CNFRefutation 0.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX206-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n008.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 07:56:43 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 0.78/1.62 % Version : CSE_E---1.7
% 0.78/1.62 % Problem : theBenchmark.p
% 0.78/1.62 % SZS status Unsatisfiable for theBenchmark.p
% 0.78/1.62 % SZS output start CNFRefutation
% 0.78/1.62 cnf(goal, negated_conjecture, (eq2(plus_not_idem(X1),bfalse)!=btrue), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goal)).
% 0.78/1.62 cnf(axiom_004, axiom, (plus_not_idem(X1)=impl(eq(x2(X1,X1),X1),eq2(btrue,bfalse))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_004)).
% 0.78/1.62 cnf(axiom_003, axiom, (x2(s(X1),X2)=s(x2(X1,X2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_003)).
% 0.78/1.62 cnf(axiom_007, axiom, (eq(s(X1),s(X2))=eq(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_007)).
% 0.78/1.62 cnf(axiom_009, axiom, (eq(s(X1),z)=bfalse), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_009)).
% 0.78/1.62 cnf(axiom_008, axiom, (eq(z,s(X1))=bfalse), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_008)).
% 0.78/1.62 cnf(axiom_011, axiom, (eq2(X1,X1)=btrue), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_011)).
% 0.78/1.62 cnf(axiom_010, axiom, (eq(X1,X1)=btrue), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_010)).
% 0.78/1.62 cnf(axiom_002, axiom, (x2(z,X1)=X1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_002)).
% 0.78/1.62 cnf(axiom, axiom, (impl(btrue,X1)=X1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom)).
% 0.78/1.62 cnf(axiom_001, axiom, (impl(bfalse,X1)=btrue), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_001)).
% 0.78/1.62 cnf(axiom_005, axiom, (eq2(bfalse,btrue)=bfalse), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_005)).
% 0.78/1.62 cnf(axiom_006, axiom, (eq2(btrue,bfalse)=bfalse), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_006)).
% 0.78/1.62 cnf(i_0_13, negated_conjecture, (eq2(plus_not_idem(X1),bfalse)!=btrue), goal).
% 0.78/1.62 cnf(i_0_14, axiom, (plus_not_idem(X1)=impl(eq(x2(X1,X1),X1),eq2(btrue,bfalse))), axiom_004).
% 0.78/1.62 cnf(i_0_15, negated_conjecture, (eq2(impl(eq(x2(X1,X1),X1),eq2(btrue,bfalse)),bfalse)!=btrue), inference(rw,[status(thm)],[i_0_13, c_0_14]), ['final']).
% 0.78/1.62 cnf(i_0_16, axiom, (x2(s(X1),X2)=s(x2(X1,X2))), axiom_003, ['final']).
% 0.78/1.62 cnf(i_0_17, axiom, (eq(s(X1),s(X2))=eq(X1,X2)), axiom_007, ['final']).
% 0.78/1.62 cnf(i_0_18, axiom, (eq(s(X1),z)=bfalse), axiom_009, ['final']).
% 0.78/1.62 cnf(i_0_19, axiom, (eq(z,s(X1))=bfalse), axiom_008, ['final']).
% 0.78/1.62 cnf(i_0_20, axiom, (eq2(X1,X1)=btrue), axiom_011, ['final']).
% 0.78/1.62 cnf(i_0_21, axiom, (eq(X1,X1)=btrue), axiom_010, ['final']).
% 0.78/1.62 cnf(i_0_22, axiom, (x2(z,X1)=X1), axiom_002, ['final']).
% 0.78/1.62 cnf(i_0_23, axiom, (impl(btrue,X1)=X1), axiom, ['final']).
% 0.78/1.62 cnf(i_0_24, axiom, (impl(bfalse,X1)=btrue), axiom_001, ['final']).
% 0.78/1.62 cnf(i_0_25, axiom, (eq2(bfalse,btrue)=bfalse), axiom_005, ['final']).
% 0.78/1.62 cnf(i_0_26, axiom, (eq2(btrue,bfalse)=bfalse), axiom_006, ['final']).
% 0.78/1.62 cnf(i_0_27, axiom, (X1=X1)).
% 0.78/1.62 cnf(i_0_28, axiom, (X1=X2|X2!=X1)).
% 0.78/1.62 cnf(i_0_29, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.78/1.62 cnf(i_0_30, axiom, (X1!=X2|eq2(X1,X3)=eq2(X2,X3))).
% 0.78/1.62 cnf(i_0_31, axiom, (X1!=X2|eq2(X3,X1)=eq2(X3,X2))).
% 0.78/1.62 cnf(i_0_32, axiom, (X1!=X2|impl(X1,X3)=impl(X2,X3))).
% 0.78/1.62 cnf(i_0_33, axiom, (X1!=X2|impl(X3,X1)=impl(X3,X2))).
% 0.78/1.62 cnf(i_0_34, axiom, (X1!=X2|eq(X1,X3)=eq(X2,X3))).
% 0.78/1.62 cnf(i_0_35, axiom, (X1!=X2|eq(X3,X1)=eq(X3,X2))).
% 0.78/1.62 cnf(i_0_36, axiom, (X1!=X2|X3(X1,X4)=X3(X2,X4))).
% 0.78/1.62 cnf(i_0_37, axiom, (X1!=X2|X3(X4,X1)=X3(X4,X2))).
% 0.78/1.62 cnf(i_0_38, axiom, (X1!=X2|s(X1)=s(X2))).
% 0.89/1.75 cnf(i_0_27, axiom, (X1=X1)).
% 0.89/1.75 cnf(i_0_28, axiom, (X1=X2|X2!=X1)).
% 0.89/1.75 cnf(i_0_29, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.89/1.75 cnf(i_0_30, axiom, (X1!=X2|eq2(X1,X3)=eq2(X2,X3))).
% 0.89/1.75 cnf(i_0_31, axiom, (X1!=X2|eq2(X3,X1)=eq2(X3,X2))).
% 0.89/1.75 cnf(i_0_32, axiom, (X1!=X2|impl(X1,X3)=impl(X2,X3))).
% 0.89/1.75 cnf(i_0_33, axiom, (X1!=X2|impl(X3,X1)=impl(X3,X2))).
% 0.89/1.75 cnf(i_0_34, axiom, (X1!=X2|eq(X1,X3)=eq(X2,X3))).
% 0.89/1.75 cnf(i_0_35, axiom, (X1!=X2|eq(X3,X1)=eq(X3,X2))).
% 0.89/1.75 cnf(i_0_36, axiom, (X1!=X2|X3(X1,X4)=X3(X2,X4))).
% 0.89/1.75 cnf(i_0_37, axiom, (X1!=X2|X3(X4,X1)=X3(X4,X2))).
% 0.89/1.75 cnf(i_0_38, axiom, (X1!=X2|s(X1)=s(X2))).
% 0.89/1.75 cnf(i_0_39, plain, (X1=X2(z,X1)), inference(scs_inference,[],[i_0_22,i_0_28])).
% 0.89/1.75 cnf(i_0_40, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=X1(z,btrue)), inference(scs_inference,[],[i_0_15,i_0_22,i_0_28,i_0_29])).
% 0.89/1.75 cnf(i_0_41, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_42, plain, (X1=impl(btrue,X1)), inference(scs_inference,[],[i_0_23,i_0_28])).
% 0.89/1.75 cnf(i_0_43, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=impl(btrue,btrue)), inference(scs_inference,[],[i_0_15,i_0_23,i_0_28,i_0_29])).
% 0.89/1.75 cnf(i_0_44, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_45, plain, (btrue=eq2(X1,X1)), inference(scs_inference,[],[i_0_20,i_0_28])).
% 0.89/1.75 cnf(i_0_46, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=eq2(X3,X3)), inference(scs_inference,[],[i_0_15,i_0_20,i_0_28,i_0_29])).
% 0.89/1.75 cnf(i_0_47, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=bfalse), inference(scs_inference,[],[i_0_15,i_0_20,i_0_28,i_0_29,i_0_30])).
% 0.89/1.75 cnf(i_0_48, plain, (btrue=eq(X1,X1)), inference(scs_inference,[],[i_0_21,i_0_28])).
% 0.89/1.75 cnf(i_0_49, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=eq(X3,X3)), inference(scs_inference,[],[i_0_15,i_0_21,i_0_28,i_0_29])).
% 0.89/1.75 cnf(i_0_50, plain, (s(X1(X2,X3))=X1(s(X2),X3)), inference(scs_inference,[],[i_0_16,i_0_28])).
% 0.89/1.75 cnf(i_0_51, plain, (X1(z,X1(s(X2),X3))=s(X1(X2,X3))), inference(scs_inference,[],[i_0_16,i_0_22,i_0_28,i_0_29])).
% 0.89/1.75 cnf(i_0_52, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_53, plain, (s(X1(X2,X3))=X1(z,X1(s(X2),X3))), inference(scs_inference,[],[i_0_51,i_0_28])).
% 0.89/1.75 cnf(i_0_54, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=impl(bfalse,X3)), inference(scs_inference,[],[i_0_15,i_0_51,i_0_24,i_0_28,i_0_29])).
% 0.89/1.75 cnf(i_0_55, plain, (eq(X1,X2)=eq(s(X1),s(X2))), inference(scs_inference,[],[i_0_17,i_0_28])).
% 0.89/1.75 cnf(i_0_56, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=eq2(btrue,bfalse)), inference(scs_inference,[],[i_0_47,i_0_17,i_0_26,i_0_28,i_0_29])).
% 0.89/1.75 cnf(i_0_57, plain, (bfalse=eq2(bfalse,btrue)), inference(scs_inference,[],[i_0_25,i_0_28])).
% 0.89/1.75 cnf(i_0_58, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=eq2(bfalse,btrue)), inference(scs_inference,[],[i_0_25,i_0_47,i_0_28,i_0_29])).
% 0.89/1.75 cnf(i_0_59, plain, (bfalse=eq(s(X1),z)), inference(scs_inference,[],[i_0_18,i_0_28])).
% 0.89/1.75 cnf(i_0_60, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=eq(s(X3),z)), inference(scs_inference,[],[i_0_18,i_0_47,i_0_28,i_0_29])).
% 0.89/1.75 cnf(i_0_61, plain, (bfalse=eq(z,s(X1))), inference(scs_inference,[],[i_0_19,i_0_28])).
% 0.89/1.75 cnf(i_0_62, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=eq(z,s(X3))), inference(scs_inference,[],[i_0_19,i_0_47,i_0_28,i_0_29])).
% 0.89/1.75 cnf(i_0_63, plain, (btrue=impl(bfalse,X1)), inference(scs_inference,[],[i_0_24,i_0_28])).
% 0.89/1.75 cnf(i_0_64, plain, (bfalse=eq2(btrue,bfalse)), inference(scs_inference,[],[i_0_26,i_0_28])).
% 0.89/1.75 cnf(i_0_65, plain, (X1(z,s(X1(X2,X3)))=X1(s(X2),X3)), inference(scs_inference,[],[i_0_22,i_0_50,i_0_29])).
% 0.89/1.75 cnf(i_0_66, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_67, plain, (X1(s(X2),X3)=X1(z,s(X1(X2,X3)))), inference(scs_inference,[],[i_0_22,i_0_50,i_0_29,i_0_28])).
% 0.89/1.75 cnf(i_0_68, plain, (impl(btrue,s(X1(X2,X3)))=X1(s(X2),X3)), inference(scs_inference,[],[i_0_23,i_0_50,i_0_29])).
% 0.89/1.75 cnf(i_0_69, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_70, plain, (X1(s(X2),X3)=impl(btrue,s(X1(X2,X3)))), inference(scs_inference,[],[i_0_23,i_0_50,i_0_29,i_0_28])).
% 0.89/1.75 cnf(i_0_71, plain, (impl(btrue,X1(s(X2),X3))=s(X1(X2,X3))), inference(scs_inference,[],[i_0_23,i_0_16,i_0_29])).
% 0.89/1.75 cnf(i_0_72, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_73, plain, (s(X1(X2,X3))=impl(btrue,X1(s(X2),X3))), inference(scs_inference,[],[i_0_23,i_0_16,i_0_29,i_0_28])).
% 0.89/1.75 cnf(i_0_74, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=X1(z,X1(z,btrue))), inference(scs_inference,[],[i_0_40,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_75, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_76, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=impl(btrue,X1(z,btrue))), inference(scs_inference,[],[i_0_40,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_77, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_78, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=X1(z,impl(btrue,btrue))), inference(scs_inference,[],[i_0_43,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_79, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_80, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=impl(btrue,impl(btrue,btrue))), inference(scs_inference,[],[i_0_43,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_81, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_82, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=X1(z,eq2(X3,X3))), inference(scs_inference,[],[i_0_46,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_83, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_84, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=impl(btrue,eq2(X3,X3))), inference(scs_inference,[],[i_0_46,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_85, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_86, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=X1(z,bfalse)), inference(scs_inference,[],[i_0_47,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_87, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_88, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=impl(btrue,bfalse)), inference(scs_inference,[],[i_0_47,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_89, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_90, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=X1(z,eq(X3,X3))), inference(scs_inference,[],[i_0_49,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_91, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_92, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=impl(btrue,eq(X3,X3))), inference(scs_inference,[],[i_0_49,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_93, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_94, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=eq(s(s(X3)),s(z))), inference(scs_inference,[],[i_0_60,i_0_17,i_0_29])).
% 0.89/1.75 cnf(i_0_95, plain, (eq(s(X1),s(X2))=eq(X1,X2)), inference(rename_variables,[],[i_0_17])).
% 0.89/1.75 cnf(i_0_96, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=X1(z,impl(bfalse,X3))), inference(scs_inference,[],[i_0_54,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_97, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_98, plain, (eq2(impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse)),bfalse)!=impl(btrue,impl(bfalse,X3))), inference(scs_inference,[],[i_0_54,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_99, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_100, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=X1(z,eq2(btrue,bfalse))), inference(scs_inference,[],[i_0_56,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_101, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_102, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=impl(btrue,eq2(btrue,bfalse))), inference(scs_inference,[],[i_0_56,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_103, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_104, plain, (eq(X1(X2,X2),X2)!=btrue), inference(scs_inference,[],[i_0_56,i_0_23,i_0_29,i_0_32])).
% 0.89/1.75 cnf(i_0_105, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=X1(z,eq2(bfalse,btrue))), inference(scs_inference,[],[i_0_58,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_106, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_107, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=impl(btrue,eq2(bfalse,btrue))), inference(scs_inference,[],[i_0_58,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_108, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_109, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=X1(z,eq(s(X3),z))), inference(scs_inference,[],[i_0_60,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_110, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_111, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=impl(btrue,eq(s(X3),z))), inference(scs_inference,[],[i_0_60,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_112, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_113, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=eq(s(z),s(s(X3)))), inference(scs_inference,[],[i_0_62,i_0_17,i_0_29])).
% 0.89/1.75 cnf(i_0_114, plain, (eq(s(X1),s(X2))=eq(X1,X2)), inference(rename_variables,[],[i_0_17])).
% 0.89/1.75 cnf(i_0_115, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=X1(z,eq(z,s(X3)))), inference(scs_inference,[],[i_0_62,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_116, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_117, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=impl(btrue,eq(z,s(X3)))), inference(scs_inference,[],[i_0_62,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_118, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_119, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=X1(z,X1(z,bfalse))), inference(scs_inference,[],[i_0_86,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_120, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_121, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=impl(btrue,X1(z,bfalse))), inference(scs_inference,[],[i_0_86,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_122, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_123, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=X1(z,impl(btrue,bfalse))), inference(scs_inference,[],[i_0_88,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_124, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_125, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=impl(btrue,impl(btrue,bfalse))), inference(scs_inference,[],[i_0_88,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_126, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_127, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=X1(z,X1(z,eq2(btrue,bfalse)))), inference(scs_inference,[],[i_0_100,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_128, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_129, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=impl(btrue,X1(z,eq2(btrue,bfalse)))), inference(scs_inference,[],[i_0_100,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_130, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_131, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=X1(z,impl(btrue,eq2(btrue,bfalse)))), inference(scs_inference,[],[i_0_102,i_0_22,i_0_29])).
% 0.89/1.75 cnf(i_0_132, plain, (X1(z,X2)=X2), inference(rename_variables,[],[i_0_22])).
% 0.89/1.75 cnf(i_0_133, plain, (impl(eq(X1(X2,X2),X2),eq2(btrue,bfalse))!=impl(btrue,impl(btrue,eq2(btrue,bfalse)))), inference(scs_inference,[],[i_0_102,i_0_23,i_0_29])).
% 0.89/1.75 cnf(i_0_134, plain, (impl(btrue,X1)=X1), inference(rename_variables,[],[i_0_23])).
% 0.89/1.75 cnf(i_0_135, plain, (eq(X1(X2,X2),X2)!=eq2(X3,X3)), inference(scs_inference,[],[i_0_104,i_0_20,i_0_29])).
% 0.89/1.75 cnf(i_0_136, plain, (eq(X1(X2,X2),X2)!=eq(X3,X3)), inference(scs_inference,[],[i_0_104,i_0_21,i_0_29])).
% 0.89/1.75 cnf(i_0_137, plain, ($false), inference(scs_inference,[],[i_0_104,i_0_21,i_0_22,i_0_29,i_0_34]), ['proof']).
% 0.89/1.75 % SZS output end CNFRefutation
% 0.89/1.75 % Total time : 1.271s
%------------------------------------------------------------------------------