%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWX024+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n019.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 : Thu Apr 10 02:51:44 AM UTC 2025
% Result : Theorem 133.29s 111.18s
% Output : CNFRefutation 133.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SWX024+1 : TPTP v9.1.0. Released v9.1.0.
% 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.35 % Computer : n019.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Apr 9 22:34:17 EDT 2025
% 0.14/0.35 % CPUTime :
% 133.29/111.18 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 133.29/111.19
% 133.29/111.19 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 133.42/111.20 %$ times_terminates > times_succeeds > times_fails > plus_terminates > plus_succeeds > plus_fails > delete_terminates > delete_succeeds > delete_fails > append_terminates > append_succeeds > append_fails > sub > member_terminates > member_succeeds > member_fails > length_terminates > length_succeeds > length_fails > @=<_terminates > @=<_succeeds > @=<_fails > @<_terminates > @<_succeeds > @<_fails > nat_terminates > nat_succeeds > nat_list_terminates > nat_list_succeeds > nat_list_fails > nat_fails > list_terminates > list_succeeds > list_fails > gr > cons > @+ > @* > ** > #nlpp > s > lh > nil > 0 > #skF_26 > #skF_49 > #skF_24 > #skF_62 > #skF_35 > #skF_11 > #skF_75 > #skF_44 > #skF_73 > #skF_80 > #skF_57 > #skF_1 > #skF_94 > #skF_91 > #skF_6 > #skF_30 > #skF_27 > #skF_17 > #skF_56 > #skF_63 > #skF_32 > #skF_37 > #skF_103 > #skF_22 > #skF_72 > #skF_64 > #skF_70 > #skF_40 > #skF_82 > #skF_52 > #skF_92 > #skF_31 > #skF_65 > #skF_4 > #skF_90 > #skF_13 > #skF_69 > #skF_34 > #skF_14 > #skF_12 > #skF_18 > #skF_85 > #skF_23 > #skF_100 > #skF_41 > #skF_74 > #skF_33 > #skF_5 > #skF_19 > #skF_102 > #skF_38 > #skF_58 > #skF_43 > #skF_10 > #skF_66 > #skF_84 > #skF_67 > #skF_2 > #skF_36 > #skF_71 > #skF_97 > #skF_7 > #skF_99 > #skF_39 > #skF_60 > #skF_9 > #skF_20 > #skF_51 > #skF_28 > #skF_86 > #skF_83 > #skF_78 > #skF_77 > #skF_81 > #skF_50 > #skF_54 > #skF_55 > #skF_93 > #skF_3 > #skF_87 > #skF_59 > #skF_95 > #skF_98 > #skF_48 > #skF_88 > #skF_68 > #skF_96 > #skF_8 > #skF_101 > #skF_25 > #skF_89 > #skF_29 > #skF_46 > #skF_42 > #skF_21 > #skF_61 > #skF_16 > #skF_45 > #skF_15 > #skF_53 > #skF_76 > #skF_79 > #skF_47
% 133.42/111.20
% 133.42/111.20 %Foreground sorts:
% 133.42/111.20
% 133.42/111.20
% 133.42/111.20 %Background operators:
% 133.42/111.20
% 133.42/111.20
% 133.42/111.20 %Foreground operators:
% 133.42/111.20 tff(times_terminates, type, times_terminates: ($i * $i * $i) > $o).
% 133.42/111.20 tff('#skF_26', type, '#skF_26': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_49', type, '#skF_49': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_24', type, '#skF_24': ($i * $i * $i) > $i).
% 133.42/111.20 tff(append_fails, type, append_fails: ($i * $i * $i) > $o).
% 133.42/111.20 tff('#skF_62', type, '#skF_62': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_35', type, '#skF_35': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_11', type, '#skF_11': ($i * $i) > $i).
% 133.42/111.20 tff(nat_fails, type, nat_fails: $i > $o).
% 133.42/111.20 tff('#skF_75', type, '#skF_75': ($i * $i) > $i).
% 133.42/111.20 tff(@=<_fails, type, @=<_fails: ($i * $i) > $o).
% 133.42/111.20 tff('#skF_44', type, '#skF_44': $i > $i).
% 133.42/111.20 tff(delete_terminates, type, delete_terminates: ($i * $i * $i) > $o).
% 133.42/111.20 tff('#skF_73', type, '#skF_73': ($i * $i) > $i).
% 133.42/111.20 tff(list_terminates, type, list_terminates: $i > $o).
% 133.42/111.20 tff('#skF_80', type, '#skF_80': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_57', type, '#skF_57': ($i * $i * $i) > $i).
% 133.42/111.20 tff(@=<_succeeds, type, @=<_succeeds: ($i * $i) > $o).
% 133.42/111.20 tff('#skF_1', type, '#skF_1': ($i * $i * $i) > $i).
% 133.42/111.20 tff(append_succeeds, type, append_succeeds: ($i * $i * $i) > $o).
% 133.42/111.20 tff('#skF_94', type, '#skF_94': $i).
% 133.42/111.20 tff(delete_fails, type, delete_fails: ($i * $i * $i) > $o).
% 133.42/111.20 tff('#skF_91', type, '#skF_91': ($i * $i) > $i).
% 133.42/111.20 tff(length_terminates, type, length_terminates: ($i * $i) > $o).
% 133.42/111.20 tff('#skF_6', type, '#skF_6': ($i * $i * $i) > $i).
% 133.42/111.20 tff(s, type, s: $i > $i).
% 133.42/111.20 tff('#skF_30', type, '#skF_30': ($i * $i) > $i).
% 133.42/111.20 tff(length_fails, type, length_fails: ($i * $i) > $o).
% 133.42/111.20 tff('#skF_27', type, '#skF_27': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_17', type, '#skF_17': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_56', type, '#skF_56': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_63', type, '#skF_63': ($i * $i) > $i).
% 133.42/111.20 tff(plus_fails, type, plus_fails: ($i * $i * $i) > $o).
% 133.42/111.20 tff('#skF_32', type, '#skF_32': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_37', type, '#skF_37': $i > $i).
% 133.42/111.20 tff(@<_terminates, type, @<_terminates: ($i * $i) > $o).
% 133.42/111.20 tff('#skF_103', type, '#skF_103': $i).
% 133.42/111.20 tff('#skF_22', type, '#skF_22': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_72', type, '#skF_72': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_64', type, '#skF_64': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_70', type, '#skF_70': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_40', type, '#skF_40': $i > $i).
% 133.42/111.20 tff('#skF_82', type, '#skF_82': ($i * $i) > $i).
% 133.42/111.20 tff(@<_succeeds, type, @<_succeeds: ($i * $i) > $o).
% 133.42/111.20 tff('#skF_52', type, '#skF_52': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_92', type, '#skF_92': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_31', type, '#skF_31': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_65', type, '#skF_65': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_4', type, '#skF_4': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_90', type, '#skF_90': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_13', type, '#skF_13': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_69', type, '#skF_69': ($i * $i) > $i).
% 133.42/111.20 tff(@*, type, @*: ($i * $i) > $i).
% 133.42/111.20 tff('#skF_34', type, '#skF_34': ($i * $i) > $i).
% 133.42/111.20 tff(@+, type, @+: ($i * $i) > $i).
% 133.42/111.20 tff('#skF_14', type, '#skF_14': ($i * $i) > $i).
% 133.42/111.20 tff(append_terminates, type, append_terminates: ($i * $i * $i) > $o).
% 133.42/111.20 tff(**, type, **: ($i * $i) > $i).
% 133.42/111.20 tff('#skF_12', type, '#skF_12': ($i * $i) > $i).
% 133.42/111.20 tff(length_succeeds, type, length_succeeds: ($i * $i) > $o).
% 133.42/111.20 tff(times_fails, type, times_fails: ($i * $i * $i) > $o).
% 133.42/111.20 tff(0, type, 0: $i).
% 133.42/111.20 tff('#skF_18', type, '#skF_18': ($i * $i) > $i).
% 133.42/111.20 tff(nat_list_terminates, type, nat_list_terminates: $i > $o).
% 133.42/111.20 tff('#skF_85', type, '#skF_85': ($i * $i) > $i).
% 133.42/111.20 tff(list_succeeds, type, list_succeeds: $i > $o).
% 133.42/111.20 tff('#skF_23', type, '#skF_23': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_100', type, '#skF_100': $i).
% 133.42/111.20 tff(plus_succeeds, type, plus_succeeds: ($i * $i * $i) > $o).
% 133.42/111.20 tff('#skF_41', type, '#skF_41': $i > $i).
% 133.42/111.20 tff('#skF_74', type, '#skF_74': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_33', type, '#skF_33': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_5', type, '#skF_5': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_19', type, '#skF_19': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_102', type, '#skF_102': $i).
% 133.42/111.20 tff('#skF_38', type, '#skF_38': $i > $i).
% 133.42/111.20 tff('#skF_58', type, '#skF_58': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_43', type, '#skF_43': $i > $i).
% 133.42/111.20 tff('#skF_10', type, '#skF_10': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_66', type, '#skF_66': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_84', type, '#skF_84': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_67', type, '#skF_67': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_2', type, '#skF_2': ($i * $i * $i) > $i).
% 133.42/111.20 tff(@=<_terminates, type, @=<_terminates: ($i * $i) > $o).
% 133.42/111.20 tff('#skF_36', type, '#skF_36': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_71', type, '#skF_71': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_97', type, '#skF_97': $i).
% 133.42/111.20 tff('#skF_7', type, '#skF_7': ($i * $i * $i) > $i).
% 133.42/111.20 tff(sub, type, sub: ($i * $i) > $o).
% 133.42/111.20 tff(nat_terminates, type, nat_terminates: $i > $o).
% 133.42/111.20 tff('#skF_99', type, '#skF_99': $i).
% 133.42/111.20 tff(nat_list_fails, type, nat_list_fails: $i > $o).
% 133.42/111.20 tff('#skF_39', type, '#skF_39': $i > $i).
% 133.42/111.20 tff('#skF_60', type, '#skF_60': ($i * $i * $i) > $i).
% 133.42/111.20 tff(lh, type, lh: $i > $i).
% 133.42/111.20 tff('#skF_9', type, '#skF_9': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_20', type, '#skF_20': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_51', type, '#skF_51': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_28', type, '#skF_28': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_86', type, '#skF_86': ($i * $i) > $i).
% 133.42/111.20 tff(cons, type, cons: ($i * $i) > $i).
% 133.42/111.20 tff('#skF_83', type, '#skF_83': ($i * $i) > $i).
% 133.42/111.20 tff(list_fails, type, list_fails: $i > $o).
% 133.42/111.20 tff('#skF_78', type, '#skF_78': $i > $i).
% 133.42/111.20 tff('#skF_77', type, '#skF_77': $i > $i).
% 133.42/111.20 tff('#skF_81', type, '#skF_81': ($i * $i) > $i).
% 133.42/111.20 tff(delete_succeeds, type, delete_succeeds: ($i * $i * $i) > $o).
% 133.42/111.20 tff('#skF_50', type, '#skF_50': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_54', type, '#skF_54': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_55', type, '#skF_55': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_93', type, '#skF_93': $i).
% 133.42/111.20 tff(nat_list_succeeds, type, nat_list_succeeds: $i > $o).
% 133.42/111.20 tff('#skF_3', type, '#skF_3': ($i * $i * $i) > $i).
% 133.42/111.20 tff(nat_succeeds, type, nat_succeeds: $i > $o).
% 133.42/111.20 tff(plus_terminates, type, plus_terminates: ($i * $i * $i) > $o).
% 133.42/111.20 tff(@<_fails, type, @<_fails: ($i * $i) > $o).
% 133.42/111.20 tff('#skF_87', type, '#skF_87': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_59', type, '#skF_59': ($i * $i * $i) > $i).
% 133.42/111.20 tff(member_fails, type, member_fails: ($i * $i) > $o).
% 133.42/111.20 tff(member_succeeds, type, member_succeeds: ($i * $i) > $o).
% 133.42/111.20 tff('#skF_95', type, '#skF_95': $i).
% 133.42/111.20 tff('#skF_98', type, '#skF_98': $i).
% 133.42/111.20 tff('#skF_48', type, '#skF_48': $i > $i).
% 133.42/111.20 tff('#skF_88', type, '#skF_88': $i > $i).
% 133.42/111.20 tff('#skF_68', type, '#skF_68': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_96', type, '#skF_96': $i).
% 133.42/111.20 tff('#skF_8', type, '#skF_8': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_101', type, '#skF_101': $i).
% 133.42/111.20 tff('#skF_25', type, '#skF_25': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_89', type, '#skF_89': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_29', type, '#skF_29': ($i * $i) > $i).
% 133.42/111.20 tff(times_succeeds, type, times_succeeds: ($i * $i * $i) > $o).
% 133.42/111.20 tff('#skF_46', type, '#skF_46': $i > $i).
% 133.42/111.20 tff(nil, type, nil: $i).
% 133.42/111.20 tff('#skF_42', type, '#skF_42': $i > $i).
% 133.42/111.20 tff('#skF_21', type, '#skF_21': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_61', type, '#skF_61': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_16', type, '#skF_16': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_45', type, '#skF_45': $i > $i).
% 133.42/111.20 tff('#skF_15', type, '#skF_15': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_53', type, '#skF_53': ($i * $i * $i) > $i).
% 133.42/111.20 tff('#skF_76', type, '#skF_76': $i > $i).
% 133.42/111.20 tff(gr, type, gr: $i > $o).
% 133.42/111.20 tff(member_terminates, type, member_terminates: ($i * $i) > $o).
% 133.42/111.20 tff('#skF_79', type, '#skF_79': ($i * $i) > $i).
% 133.42/111.20 tff('#skF_47', type, '#skF_47': $i > $i).
% 133.42/111.20
% 133.42/111.22 tff(f_1513, negated_conjecture, ~(![Xx, Xl1, Xl2, Xl3]: ((append_succeeds(Xl1, Xl2, Xl3) & member_succeeds(Xx, Xl3)) => (member_succeeds(Xx, Xl1) | member_succeeds(Xx, Xl2)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', lemma-(append:member:3))).
% 133.42/111.22 tff(f_1504, axiom, ((![Xl1, Xl2, Xl3]: (((?[Xx4, Xx5, Xx6]: ((((Xl1 = cons(Xx4, Xx5)) & (Xl3 = cons(Xx4, Xx6))) & append_succeeds(Xx5, Xl2, Xx6)) & (![Xx]: (member_succeeds(Xx, Xx6) => (member_succeeds(Xx, Xx5) | member_succeeds(Xx, Xl2)))))) | ((Xl1 = nil) & (Xl3 = Xl2))) => (![Xx]: (member_succeeds(Xx, Xl3) => (member_succeeds(Xx, Xl1) | member_succeeds(Xx, Xl2)))))) => (![Xl1, Xl2, Xl3]: (append_succeeds(Xl1, Xl2, Xl3) => (![Xx]: (member_succeeds(Xx, Xl3) => (member_succeeds(Xx, Xl1) | member_succeeds(Xx, Xl2))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', induction)).
% 133.42/111.22 tff(f_344, axiom, (![Xx1, Xx2]: (member_fails(Xx1, Xx2) <=> ((![Xx3, Xx4]: (~(Xx2 = cons(Xx3, Xx4)) | member_fails(Xx1, Xx4))) & (![Xx5]: ~(Xx2 = cons(Xx1, Xx5)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', id46)).
% 133.42/111.22 tff(f_256, axiom, (![Xx1, Xx2]: (length_fails(Xx1, Xx2) <=> ((![Xx3, Xx4, Xx5]: ((~(Xx1 = cons(Xx3, Xx4)) | ~(Xx2 = s(Xx5))) | length_fails(Xx4, Xx5))) & (~(Xx1 = nil) | ~(Xx2 = 0))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', id40)).
% 133.42/111.22 tff(f_638, axiom, (![Xx1]: (nat_terminates(Xx1) <=> ((![Xx2]: ($true & (~(Xx1 = s(Xx2)) | nat_terminates(Xx2)))) & $true))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', id68)).
% 133.42/111.22 tff(f_45, axiom, (![Xx11, Xx12, Xx13]: ~(s(Xx11) = cons(Xx12, Xx13))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', id7)).
% 133.42/111.22 tff(f_1211, axiom, (![Xx, Xl]: (list_succeeds(Xl) => (member_succeeds(Xx, Xl) | member_fails(Xx, Xl)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', corollary-(member:termination))).
% 133.42/111.22 tff(f_364, axiom, (![Xx1]: (list_succeeds(Xx1) <=> ((?[Xx2, Xx3]: ((Xx1 = cons(Xx2, Xx3)) & list_succeeds(Xx3))) | (Xx1 = nil)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', id48)).
% 133.42/111.22 tff(f_385, axiom, (![Xx1]: (list_terminates(Xx1) <=> ((![Xx2, Xx3]: ($true & (~(Xx1 = cons(Xx2, Xx3)) | list_terminates(Xx3)))) & $true))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', id50)).
% 133.42/111.22 tff(f_38, axiom, (![Xx7, Xx8]: ~(nil = cons(Xx7, Xx8))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', id5)).
% 133.42/111.22 tff(f_120, axiom, (![Xx35]: (list_terminates(Xx35) => (list_succeeds(Xx35) | list_fails(Xx35)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', id23)).
% 133.42/111.22 tff(f_1228, axiom, (![Xl1, Xl2, Xl3]: (append_succeeds(Xl1, Xl2, Xl3) => list_succeeds(Xl1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', lemma-(append:types:1))).
% 133.42/111.22 tff(f_1346, axiom, (![Xl]: (list_succeeds(Xl) => (?[Xn]: length_succeeds(Xl, Xn)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', lemma-(length:existence))).
% 133.42/111.22 tff(f_1180, axiom, (![Xl, Xn]: (list_succeeds(Xl) => ((lh(Xl) = Xn) <=> length_succeeds(Xl, Xn)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', lh/1)).
% 133.42/111.22 tff(f_81, axiom, (![Xx28, Xx29]: ~(length_succeeds(Xx28, Xx29) & length_fails(Xx28, Xx29))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', id16)).
% 133.42/111.22 tff(f_1224, axiom, (![Xx, Xy, Xz, Xl]: ((member_succeeds(Xx, cons(Xy, Xl)) & ~(Xx = Xy)) => member_succeeds(Xx, Xl))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', lemma-(member:cons))).
% 133.42/111.22 tff(f_332, axiom, (![Xx1, Xx2]: (member_succeeds(Xx1, Xx2) <=> ((?[Xx3, Xx4]: ((Xx2 = cons(Xx3, Xx4)) & member_succeeds(Xx1, Xx4))) | (?[Xx5]: (Xx2 = cons(Xx1, Xx5)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', id45)).
% 133.42/111.22 tff(c_770, plain, (~member_succeeds('#skF_100', '#skF_101')), inference(cnfTransformation, [status(thm)], [f_1513])).
% 133.42/111.22 tff(c_768, plain, (~member_succeeds('#skF_100', '#skF_102')), inference(cnfTransformation, [status(thm)], [f_1513])).
% 133.42/111.22 tff(c_774, plain, (append_succeeds('#skF_101', '#skF_102', '#skF_103')), inference(cnfTransformation, [status(thm)], [f_1513])).
% 133.42/111.22 tff(c_772, plain, (member_succeeds('#skF_100', '#skF_103')), inference(cnfTransformation, [status(thm)], [f_1513])).
% 133.42/111.22 tff(c_748, plain, (![Xx_751, Xl2_748, Xl1_747, Xl3_749]: (~member_succeeds('#skF_99', '#skF_93') | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(cnfTransformation, [status(thm)], [f_1504])).
% 133.42/111.22 tff(c_226785, plain, (~member_succeeds('#skF_99', '#skF_93')), inference(splitLeft, [status(thm)], [c_748])).
% 133.42/111.22 tff(c_750, plain, (![Xx_751, Xl2_748, Xl1_747, Xl3_749]: (member_succeeds('#skF_99', '#skF_95') | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(cnfTransformation, [status(thm)], [f_1504])).
% 133.42/111.22 tff(c_224815, plain, (member_succeeds('#skF_99', '#skF_95')), inference(splitLeft, [status(thm)], [c_750])).
% 133.42/111.22 tff(c_756, plain, (![Xx_751, Xl2_748, Xl1_747, Xl3_749]: (cons('#skF_96', '#skF_98')='#skF_95' | '#skF_94'='#skF_95' | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(cnfTransformation, [status(thm)], [f_1504])).
% 133.42/111.22 tff(c_260925, plain, ('#skF_94'='#skF_95'), inference(splitLeft, [status(thm)], [c_756])).
% 133.42/111.22 tff(c_746, plain, (![Xx_751, Xl2_748, Xl1_747, Xl3_749]: (~member_succeeds('#skF_99', '#skF_94') | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(cnfTransformation, [status(thm)], [f_1504])).
% 133.42/111.22 tff(c_224424, plain, (~member_succeeds('#skF_99', '#skF_94')), inference(splitLeft, [status(thm)], [c_746])).
% 133.42/111.22 tff(c_260933, plain, (~member_succeeds('#skF_99', '#skF_95')), inference(demodulation, [status(thm), theory('equality')], [c_260925, c_224424])).
% 133.42/111.22 tff(c_260936, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_224815, c_260933])).
% 133.42/111.22 tff(c_260938, plain, ('#skF_94'!='#skF_95'), inference(splitRight, [status(thm)], [c_756])).
% 133.42/111.22 tff(c_758, plain, (![Xx_751, Xl2_748, Xl1_747, Xl3_749]: (cons('#skF_96', '#skF_97')='#skF_93' | '#skF_94'='#skF_95' | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(cnfTransformation, [status(thm)], [f_1504])).
% 133.42/111.22 tff(c_261921, plain, (![Xx_751, Xl2_748, Xl1_747, Xl3_749]: (cons('#skF_96', '#skF_97')='#skF_93' | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(negUnitSimplification, [status(thm)], [c_260938, c_758])).
% 133.42/111.22 tff(c_261922, plain, (cons('#skF_96', '#skF_97')='#skF_93'), inference(splitLeft, [status(thm)], [c_261921])).
% 133.42/111.22 tff(c_194, plain, (![Xx1_185, Xx5_195]: (~member_fails(Xx1_185, cons(Xx1_185, Xx5_195)))), inference(cnfTransformation, [status(thm)], [f_344])).
% 133.42/111.22 tff(c_262179, plain, (~member_fails('#skF_96', '#skF_93')), inference(superposition, [status(thm), theory('equality')], [c_261922, c_194])).
% 133.42/111.22 tff(c_754, plain, (![Xx_751, Xl2_748, Xl1_747, Xl3_749]: (append_succeeds('#skF_97', '#skF_94', '#skF_98') | '#skF_94'='#skF_95' | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(cnfTransformation, [status(thm)], [f_1504])).
% 133.42/111.22 tff(c_252450, plain, ('#skF_94'='#skF_95'), inference(splitLeft, [status(thm)], [c_754])).
% 133.42/111.22 tff(c_252456, plain, (~member_succeeds('#skF_99', '#skF_95')), inference(demodulation, [status(thm), theory('equality')], [c_252450, c_224424])).
% 133.42/111.22 tff(c_252459, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_224815, c_252456])).
% 133.42/111.22 tff(c_252461, plain, ('#skF_94'!='#skF_95'), inference(splitRight, [status(thm)], [c_754])).
% 133.42/111.22 tff(c_204186, plain, (![Xx1_9669, Xx2_9670]: (cons('#skF_13'(Xx1_9669, Xx2_9670), '#skF_14'(Xx1_9669, Xx2_9670))=Xx1_9669 | nil=Xx1_9669 | length_fails(Xx1_9669, Xx2_9670))), inference(cnfTransformation, [status(thm)], [f_256])).
% 133.42/111.22 tff(c_1156, plain, (![Xx1_881]: (s('#skF_78'(Xx1_881))=Xx1_881 | nat_terminates(Xx1_881))), inference(cnfTransformation, [status(thm)], [f_638])).
% 133.42/111.22 tff(c_14, plain, (![Xx11_9, Xx12_10, Xx13_11]: (s(Xx11_9)!=cons(Xx12_10, Xx13_11))), inference(cnfTransformation, [status(thm)], [f_45])).
% 133.42/111.22 tff(c_1197, plain, (![Xx12_10, Xx13_11, Xx1_881]: (cons(Xx12_10, Xx13_11)!=Xx1_881 | nat_terminates(Xx1_881))), inference(superposition, [status(thm), theory('equality')], [c_1156, c_14])).
% 133.42/111.22 tff(c_204414, plain, (![Xx1_9669, Xx2_9670]: (nat_terminates(Xx1_9669) | nil=Xx1_9669 | length_fails(Xx1_9669, Xx2_9670))), inference(superposition, [status(thm), theory('equality')], [c_204186, c_1197])).
% 133.42/111.22 tff(c_638, plain, (![Xx_613, Xl_614]: (member_fails(Xx_613, Xl_614) | member_succeeds(Xx_613, Xl_614) | ~list_succeeds(Xl_614))), inference(cnfTransformation, [status(thm)], [f_1211])).
% 133.42/111.22 tff(c_226794, plain, (member_fails('#skF_99', '#skF_93') | ~list_succeeds('#skF_93')), inference(resolution, [status(thm)], [c_638, c_226785])).
% 133.42/111.22 tff(c_226795, plain, (~list_succeeds('#skF_93')), inference(splitLeft, [status(thm)], [c_226794])).
% 133.42/111.22 tff(c_241726, plain, ('#skF_94'='#skF_95'), inference(splitLeft, [status(thm)], [c_758])).
% 133.42/111.22 tff(c_241732, plain, (~member_succeeds('#skF_99', '#skF_95')), inference(demodulation, [status(thm), theory('equality')], [c_241726, c_224424])).
% 133.42/111.22 tff(c_241735, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_224815, c_241732])).
% 133.42/111.22 tff(c_241736, plain, (![Xx_751, Xl2_748, Xl1_747, Xl3_749]: (cons('#skF_96', '#skF_97')='#skF_93' | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(splitRight, [status(thm)], [c_758])).
% 133.42/111.22 tff(c_242189, plain, (cons('#skF_96', '#skF_97')='#skF_93'), inference(splitLeft, [status(thm)], [c_241736])).
% 133.42/111.22 tff(c_214, plain, (![Xx3_213, Xx2_212]: (~list_succeeds(Xx3_213) | list_succeeds(cons(Xx2_212, Xx3_213)))), inference(cnfTransformation, [status(thm)], [f_364])).
% 133.42/111.22 tff(c_242398, plain, (~list_succeeds('#skF_97') | list_succeeds('#skF_93')), inference(superposition, [status(thm), theory('equality')], [c_242189, c_214])).
% 133.42/111.22 tff(c_242429, plain, (~list_succeeds('#skF_97')), inference(negUnitSimplification, [status(thm)], [c_226795, c_242398])).
% 133.42/111.22 tff(c_56598, plain, (![Xx1_3635]: (cons('#skF_41'(Xx1_3635), '#skF_42'(Xx1_3635))=Xx1_3635 | list_terminates(Xx1_3635))), inference(cnfTransformation, [status(thm)], [f_385])).
% 133.42/111.22 tff(c_10, plain, (![Xx7_5, Xx8_6]: (cons(Xx7_5, Xx8_6)!=nil)), inference(cnfTransformation, [status(thm)], [f_38])).
% 133.42/111.22 tff(c_56704, plain, (![Xx1_3636]: (nil!=Xx1_3636 | list_terminates(Xx1_3636))), inference(superposition, [status(thm), theory('equality')], [c_56598, c_10])).
% 133.42/111.22 tff(c_52, plain, (![Xx35_44]: (list_fails(Xx35_44) | list_succeeds(Xx35_44) | ~list_terminates(Xx35_44))), inference(cnfTransformation, [status(thm)], [f_120])).
% 133.42/111.22 tff(c_56714, plain, (![Xx1_3636]: (list_fails(Xx1_3636) | list_succeeds(Xx1_3636) | nil!=Xx1_3636)), inference(resolution, [status(thm)], [c_56704, c_52])).
% 133.42/111.22 tff(c_226810, plain, (list_fails('#skF_93') | nil!='#skF_93'), inference(resolution, [status(thm)], [c_56714, c_226795])).
% 133.42/111.22 tff(c_226848, plain, (nil!='#skF_93'), inference(splitLeft, [status(thm)], [c_226810])).
% 133.42/111.22 tff(c_762, plain, (![Xx_751, Xl2_748, Xl1_747, Xl3_749]: (append_succeeds('#skF_97', '#skF_94', '#skF_98') | nil='#skF_93' | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(cnfTransformation, [status(thm)], [f_1504])).
% 133.42/111.22 tff(c_242621, plain, (![Xx_751, Xl2_748, Xl1_747, Xl3_749]: (append_succeeds('#skF_97', '#skF_94', '#skF_98') | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(negUnitSimplification, [status(thm)], [c_226848, c_762])).
% 133.42/111.22 tff(c_242622, plain, (append_succeeds('#skF_97', '#skF_94', '#skF_98')), inference(splitLeft, [status(thm)], [c_242621])).
% 133.42/111.22 tff(c_644, plain, (![Xl1_621, Xl2_622, Xl3_623]: (list_succeeds(Xl1_621) | ~append_succeeds(Xl1_621, Xl2_622, Xl3_623))), inference(cnfTransformation, [status(thm)], [f_1228])).
% 133.42/111.22 tff(c_242832, plain, (list_succeeds('#skF_97')), inference(resolution, [status(thm)], [c_242622, c_644])).
% 133.42/111.22 tff(c_242852, plain, $false, inference(negUnitSimplification, [status(thm)], [c_242429, c_242832])).
% 133.42/111.22 tff(c_243060, plain, (![Xx_10680, Xl2_10681, Xl1_10682, Xl3_10683]: (member_succeeds(Xx_10680, Xl2_10681) | member_succeeds(Xx_10680, Xl1_10682) | ~member_succeeds(Xx_10680, Xl3_10683) | ~append_succeeds(Xl1_10682, Xl2_10681, Xl3_10683))), inference(splitRight, [status(thm)], [c_242621])).
% 133.42/111.22 tff(c_243240, plain, (![Xl2_10684, Xl1_10685]: (member_succeeds('#skF_100', Xl2_10684) | member_succeeds('#skF_100', Xl1_10685) | ~append_succeeds(Xl1_10685, Xl2_10684, '#skF_103'))), inference(resolution, [status(thm)], [c_772, c_243060])).
% 133.42/111.22 tff(c_243251, plain, (member_succeeds('#skF_100', '#skF_102') | member_succeeds('#skF_100', '#skF_101')), inference(resolution, [status(thm)], [c_774, c_243240])).
% 133.42/111.22 tff(c_243258, plain, $false, inference(negUnitSimplification, [status(thm)], [c_770, c_768, c_243251])).
% 133.42/111.22 tff(c_243263, plain, (![Xx_10686, Xl2_10687, Xl1_10688, Xl3_10689]: (member_succeeds(Xx_10686, Xl2_10687) | member_succeeds(Xx_10686, Xl1_10688) | ~member_succeeds(Xx_10686, Xl3_10689) | ~append_succeeds(Xl1_10688, Xl2_10687, Xl3_10689))), inference(splitRight, [status(thm)], [c_241736])).
% 133.42/111.22 tff(c_243652, plain, (![Xl2_10697, Xl1_10698]: (member_succeeds('#skF_100', Xl2_10697) | member_succeeds('#skF_100', Xl1_10698) | ~append_succeeds(Xl1_10698, Xl2_10697, '#skF_103'))), inference(resolution, [status(thm)], [c_772, c_243263])).
% 133.42/111.22 tff(c_243663, plain, (member_succeeds('#skF_100', '#skF_102') | member_succeeds('#skF_100', '#skF_101')), inference(resolution, [status(thm)], [c_774, c_243652])).
% 133.42/111.22 tff(c_243670, plain, $false, inference(negUnitSimplification, [status(thm)], [c_770, c_768, c_243663])).
% 133.42/111.22 tff(c_243672, plain, (nil='#skF_93'), inference(splitRight, [status(thm)], [c_226810])).
% 133.42/111.22 tff(c_212, plain, (list_succeeds(nil)), inference(cnfTransformation, [status(thm)], [f_364])).
% 133.42/111.22 tff(c_243922, plain, (list_succeeds('#skF_93')), inference(demodulation, [status(thm), theory('equality')], [c_243672, c_212])).
% 133.42/111.22 tff(c_243927, plain, $false, inference(negUnitSimplification, [status(thm)], [c_226795, c_243922])).
% 133.42/111.22 tff(c_243929, plain, (list_succeeds('#skF_93')), inference(splitRight, [status(thm)], [c_226794])).
% 133.42/111.22 tff(c_694, plain, (![Xl_674]: (length_succeeds(Xl_674, '#skF_88'(Xl_674)) | ~list_succeeds(Xl_674))), inference(cnfTransformation, [status(thm)], [f_1346])).
% 133.42/111.22 tff(c_2014, plain, (![Xl_988, Xn_989]: (lh(Xl_988)=Xn_989 | ~length_succeeds(Xl_988, Xn_989) | ~list_succeeds(Xl_988))), inference(cnfTransformation, [status(thm)], [f_1180])).
% 133.42/111.22 tff(c_2024, plain, (![Xl_674]: (lh(Xl_674)='#skF_88'(Xl_674) | ~list_succeeds(Xl_674))), inference(resolution, [status(thm)], [c_694, c_2014])).
% 133.42/111.22 tff(c_243977, plain, (lh('#skF_93')='#skF_88'('#skF_93')), inference(resolution, [status(thm)], [c_243929, c_2024])).
% 133.42/111.22 tff(c_618, plain, (![Xl_595]: (length_succeeds(Xl_595, lh(Xl_595)) | ~list_succeeds(Xl_595))), inference(cnfTransformation, [status(thm)], [f_1180])).
% 133.42/111.22 tff(c_1345, plain, (![Xx28_899, Xx29_900]: (~length_fails(Xx28_899, Xx29_900) | ~length_succeeds(Xx28_899, Xx29_900))), inference(cnfTransformation, [status(thm)], [f_81])).
% 133.42/111.22 tff(c_1356, plain, (![Xl_595]: (~length_fails(Xl_595, lh(Xl_595)) | ~list_succeeds(Xl_595))), inference(resolution, [status(thm)], [c_618, c_1345])).
% 133.42/111.22 tff(c_244489, plain, (~length_fails('#skF_93', '#skF_88'('#skF_93')) | ~list_succeeds('#skF_93')), inference(superposition, [status(thm), theory('equality')], [c_243977, c_1356])).
% 133.42/111.22 tff(c_244585, plain, (~length_fails('#skF_93', '#skF_88'('#skF_93'))), inference(demodulation, [status(thm), theory('equality')], [c_243929, c_244489])).
% 133.42/111.22 tff(c_245477, plain, (nat_terminates('#skF_93') | nil='#skF_93'), inference(resolution, [status(thm)], [c_204414, c_244585])).
% 133.42/111.22 tff(c_245516, plain, (nil='#skF_93'), inference(splitLeft, [status(thm)], [c_245477])).
% 133.42/111.22 tff(c_245760, plain, (![Xx7_5, Xx8_6]: (cons(Xx7_5, Xx8_6)!='#skF_93')), inference(demodulation, [status(thm), theory('equality')], [c_245516, c_10])).
% 133.42/111.22 tff(c_252855, plain, (![Xx_10852, Xl2_10853, Xl1_10854, Xl3_10855]: (member_succeeds(Xx_10852, Xl2_10853) | member_succeeds(Xx_10852, Xl1_10854) | ~member_succeeds(Xx_10852, Xl3_10855) | ~append_succeeds(Xl1_10854, Xl2_10853, Xl3_10855))), inference(negUnitSimplification, [status(thm)], [c_252461, c_245760, c_758])).
% 133.42/111.22 tff(c_253256, plain, (![Xl2_10856, Xl1_10857]: (member_succeeds('#skF_100', Xl2_10856) | member_succeeds('#skF_100', Xl1_10857) | ~append_succeeds(Xl1_10857, Xl2_10856, '#skF_103'))), inference(resolution, [status(thm)], [c_772, c_252855])).
% 133.42/111.22 tff(c_253267, plain, (member_succeeds('#skF_100', '#skF_102') | member_succeeds('#skF_100', '#skF_101')), inference(resolution, [status(thm)], [c_774, c_253256])).
% 133.42/111.22 tff(c_253274, plain, $false, inference(negUnitSimplification, [status(thm)], [c_770, c_768, c_253267])).
% 133.42/111.22 tff(c_253276, plain, (nil!='#skF_93'), inference(splitRight, [status(thm)], [c_245477])).
% 133.42/111.22 tff(c_760, plain, (![Xl3_749, Xx_746, Xx_751, Xl2_748, Xl1_747]: (member_succeeds(Xx_746, '#skF_94') | member_succeeds(Xx_746, '#skF_97') | ~member_succeeds(Xx_746, '#skF_98') | nil='#skF_93' | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(cnfTransformation, [status(thm)], [f_1504])).
% 133.42/111.22 tff(c_263256, plain, (![Xl3_749, Xx_746, Xx_751, Xl2_748, Xl1_747]: (member_succeeds(Xx_746, '#skF_94') | member_succeeds(Xx_746, '#skF_97') | ~member_succeeds(Xx_746, '#skF_98') | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(negUnitSimplification, [status(thm)], [c_253276, c_760])).
% 133.42/111.22 tff(c_263482, plain, (![Xx_11014, Xl2_11015, Xl1_11016, Xl3_11017]: (member_succeeds(Xx_11014, Xl2_11015) | member_succeeds(Xx_11014, Xl1_11016) | ~member_succeeds(Xx_11014, Xl3_11017) | ~append_succeeds(Xl1_11016, Xl2_11015, Xl3_11017))), inference(splitLeft, [status(thm)], [c_263256])).
% 133.42/111.22 tff(c_263754, plain, (![Xl2_11019, Xl1_11020]: (member_succeeds('#skF_100', Xl2_11019) | member_succeeds('#skF_100', Xl1_11020) | ~append_succeeds(Xl1_11020, Xl2_11019, '#skF_103'))), inference(resolution, [status(thm)], [c_772, c_263482])).
% 133.42/111.22 tff(c_263765, plain, (member_succeeds('#skF_100', '#skF_102') | member_succeeds('#skF_100', '#skF_101')), inference(resolution, [status(thm)], [c_774, c_263754])).
% 133.42/111.22 tff(c_263772, plain, $false, inference(negUnitSimplification, [status(thm)], [c_770, c_768, c_263765])).
% 133.42/111.22 tff(c_263987, plain, (![Xx_11021]: (member_succeeds(Xx_11021, '#skF_94') | member_succeeds(Xx_11021, '#skF_97') | ~member_succeeds(Xx_11021, '#skF_98'))), inference(splitRight, [status(thm)], [c_263256])).
% 133.42/111.22 tff(c_264007, plain, (member_succeeds('#skF_99', '#skF_97') | ~member_succeeds('#skF_99', '#skF_98')), inference(resolution, [status(thm)], [c_263987, c_224424])).
% 133.42/111.22 tff(c_268323, plain, (~member_succeeds('#skF_99', '#skF_98')), inference(splitLeft, [status(thm)], [c_264007])).
% 133.42/111.22 tff(c_260937, plain, (![Xx_751, Xl2_748, Xl1_747, Xl3_749]: (cons('#skF_96', '#skF_98')='#skF_95' | member_succeeds(Xx_751, Xl2_748) | member_succeeds(Xx_751, Xl1_747) | ~member_succeeds(Xx_751, Xl3_749) | ~append_succeeds(Xl1_747, Xl2_748, Xl3_749))), inference(splitRight, [status(thm)], [c_756])).
% 133.42/111.22 tff(c_261350, plain, (cons('#skF_96', '#skF_98')='#skF_95'), inference(splitLeft, [status(thm)], [c_260937])).
% 133.42/111.22 tff(c_642, plain, (![Xx_617, Xl_620, Xy_618]: (member_succeeds(Xx_617, Xl_620) | Xy_618=Xx_617 | ~member_succeeds(Xx_617, cons(Xy_618, Xl_620)))), inference(cnfTransformation, [status(thm)], [f_1224])).
% 133.42/111.22 tff(c_320430, plain, (![Xx_12282]: (member_succeeds(Xx_12282, '#skF_98') | Xx_12282='#skF_96' | ~member_succeeds(Xx_12282, '#skF_95'))), inference(superposition, [status(thm), theory('equality')], [c_261350, c_642])).
% 133.42/111.22 tff(c_320458, plain, (member_succeeds('#skF_99', '#skF_98') | '#skF_99'='#skF_96'), inference(resolution, [status(thm)], [c_224815, c_320430])).
% 133.42/111.22 tff(c_320501, plain, ('#skF_99'='#skF_96'), inference(negUnitSimplification, [status(thm)], [c_268323, c_320458])).
% 133.42/111.22 tff(c_243928, plain, (member_fails('#skF_99', '#skF_93')), inference(splitRight, [status(thm)], [c_226794])).
% 133.42/111.22 tff(c_320522, plain, (member_fails('#skF_96', '#skF_93')), inference(demodulation, [status(thm), theory('equality')], [c_320501, c_243928])).
% 133.42/111.22 tff(c_320542, plain, $false, inference(negUnitSimplification, [status(thm)], [c_262179, c_320522])).
% 133.42/111.22 tff(c_320543, plain, (member_succeeds('#skF_99', '#skF_97')), inference(splitRight, [status(thm)], [c_264007])).
% 133.42/111.22 tff(c_192, plain, (![Xx1_174, Xx4_183, Xx3_182]: (~member_succeeds(Xx1_174, Xx4_183) | member_succeeds(Xx1_174, cons(Xx3_182, Xx4_183)))), inference(cnfTransformation, [status(thm)], [f_332])).
% 133.42/111.22 tff(c_262127, plain, (![Xx1_174]: (~member_succeeds(Xx1_174, '#skF_97') | member_succeeds(Xx1_174, '#skF_93'))), inference(superposition, [status(thm), theory('equality')], [c_261922, c_192])).
% 133.42/111.22 tff(c_320547, plain, (member_succeeds('#skF_99', '#skF_93')), inference(resolution, [status(thm)], [c_320543, c_262127])).
% 133.42/111.22 tff(c_320563, plain, $false, inference(negUnitSimplification, [status(thm)], [c_226785, c_320547])).
% 133.42/111.22 tff(c_320606, plain, (![Xx_12285, Xl2_12286, Xl1_12287, Xl3_12288]: (member_succeeds(Xx_12285, Xl2_12286) | member_succeeds(Xx_12285, Xl1_12287) | ~member_succeeds(Xx_12285, Xl3_12288) | ~append_succeeds(Xl1_12287, Xl2_12286, Xl3_12288))), inference(splitRight, [status(thm)], [c_261921])).
% 133.42/111.22 tff(c_320813, plain, (![Xl2_12289, Xl1_12290]: (member_succeeds('#skF_100', Xl2_12289) | member_succeeds('#skF_100', Xl1_12290) | ~append_succeeds(Xl1_12290, Xl2_12289, '#skF_103'))), inference(resolution, [status(thm)], [c_772, c_320606])).
% 133.42/111.22 tff(c_320824, plain, (member_succeeds('#skF_100', '#skF_102') | member_succeeds('#skF_100', '#skF_101')), inference(resolution, [status(thm)], [c_774, c_320813])).
% 133.42/111.22 tff(c_320831, plain, $false, inference(negUnitSimplification, [status(thm)], [c_770, c_768, c_320824])).
% 133.42/111.22 tff(c_320992, plain, (![Xx_12291, Xl2_12292, Xl1_12293, Xl3_12294]: (member_succeeds(Xx_12291, Xl2_12292) | member_succeeds(Xx_12291, Xl1_12293) | ~member_succeeds(Xx_12291, Xl3_12294) | ~append_succeeds(Xl1_12293, Xl2_12292, Xl3_12294))), inference(splitRight, [status(thm)], [c_260937])).
% 133.42/111.22 tff(c_321183, plain, (![Xl2_12295, Xl1_12296]: (member_succeeds('#skF_100', Xl2_12295) | member_succeeds('#skF_100', Xl1_12296) | ~append_succeeds(Xl1_12296, Xl2_12295, '#skF_103'))), inference(resolution, [status(thm)], [c_772, c_320992])).
% 133.42/111.22 tff(c_321194, plain, (member_succeeds('#skF_100', '#skF_102') | member_succeeds('#skF_100', '#skF_101')), inference(resolution, [status(thm)], [c_774, c_321183])).
% 133.42/111.22 tff(c_321201, plain, $false, inference(negUnitSimplification, [status(thm)], [c_770, c_768, c_321194])).
% 133.42/111.22 tff(c_321239, plain, (![Xx_12298, Xl2_12299, Xl1_12300, Xl3_12301]: (member_succeeds(Xx_12298, Xl2_12299) | member_succeeds(Xx_12298, Xl1_12300) | ~member_succeeds(Xx_12298, Xl3_12301) | ~append_succeeds(Xl1_12300, Xl2_12299, Xl3_12301))), inference(splitRight, [status(thm)], [c_748])).
% 133.42/111.22 tff(c_321421, plain, (![Xl2_12304, Xl1_12305]: (member_succeeds('#skF_100', Xl2_12304) | member_succeeds('#skF_100', Xl1_12305) | ~append_succeeds(Xl1_12305, Xl2_12304, '#skF_103'))), inference(resolution, [status(thm)], [c_772, c_321239])).
% 133.42/111.22 tff(c_321432, plain, (member_succeeds('#skF_100', '#skF_102') | member_succeeds('#skF_100', '#skF_101')), inference(resolution, [status(thm)], [c_774, c_321421])).
% 133.42/111.22 tff(c_321439, plain, $false, inference(negUnitSimplification, [status(thm)], [c_770, c_768, c_321432])).
% 133.42/111.22 tff(c_321469, plain, (![Xx_12306, Xl2_12307, Xl1_12308, Xl3_12309]: (member_succeeds(Xx_12306, Xl2_12307) | member_succeeds(Xx_12306, Xl1_12308) | ~member_succeeds(Xx_12306, Xl3_12309) | ~append_succeeds(Xl1_12308, Xl2_12307, Xl3_12309))), inference(splitRight, [status(thm)], [c_750])).
% 133.42/111.22 tff(c_321601, plain, (![Xl2_12310, Xl1_12311]: (member_succeeds('#skF_100', Xl2_12310) | member_succeeds('#skF_100', Xl1_12311) | ~append_succeeds(Xl1_12311, Xl2_12310, '#skF_103'))), inference(resolution, [status(thm)], [c_772, c_321469])).
% 133.42/111.22 tff(c_321612, plain, (member_succeeds('#skF_100', '#skF_102') | member_succeeds('#skF_100', '#skF_101')), inference(resolution, [status(thm)], [c_774, c_321601])).
% 133.42/111.22 tff(c_321619, plain, $false, inference(negUnitSimplification, [status(thm)], [c_770, c_768, c_321612])).
% 133.42/111.22 tff(c_321657, plain, (![Xx_12313, Xl2_12314, Xl1_12315, Xl3_12316]: (member_succeeds(Xx_12313, Xl2_12314) | member_succeeds(Xx_12313, Xl1_12315) | ~member_succeeds(Xx_12313, Xl3_12316) | ~append_succeeds(Xl1_12315, Xl2_12314, Xl3_12316))), inference(splitRight, [status(thm)], [c_746])).
% 133.42/111.22 tff(c_321812, plain, (![Xl2_12319, Xl1_12320]: (member_succeeds('#skF_100', Xl2_12319) | member_succeeds('#skF_100', Xl1_12320) | ~append_succeeds(Xl1_12320, Xl2_12319, '#skF_103'))), inference(resolution, [status(thm)], [c_772, c_321657])).
% 133.42/111.22 tff(c_321823, plain, (member_succeeds('#skF_100', '#skF_102') | member_succeeds('#skF_100', '#skF_101')), inference(resolution, [status(thm)], [c_774, c_321812])).
% 133.42/111.22 tff(c_321830, plain, $false, inference(negUnitSimplification, [status(thm)], [c_770, c_768, c_321823])).
% 133.42/111.22 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------