%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX220+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n021.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:46 PM UTC 2026
% Result : Theorem 83.14s 41.83s
% Output : CNFRefutation 89.15s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_140)
% Comments :
%------------------------------------------------------------------------------
fof(goal_032,conjecture,
? [X11] : tc(nil,X11,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_032) ).
fof(axiom_028,axiom,
! [X1,X6,X11] :
( X6 != arr(proj1Arr(X6),proj2Arr(X6))
=> ~ tc(X1,lam(X11),X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_028) ).
fof(axiom_030,axiom,
! [X1,X6,X3] :
( index(X1,X3) = nothing
=> ~ tc(X1,var(X3),X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_030) ).
fof(axiom_027,axiom,
! [X1,X6,X9,X2,X10] :
( tc(X1,app(X9,X2,X10),X6)
<=> ( tc(X1,X9,arr(X10,X6))
& tc(X1,X2,X10) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_027) ).
fof(axiom_029,axiom,
! [X1,X11,X12,X13] :
( tc(X1,lam(X11),arr(X12,X13))
<=> tc(cons(X12,X1),X11,X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_029) ).
fof(axiom_031,axiom,
! [X1,X6,X3,X14] :
( index(X1,X3) = just(X14)
=> ( tc(X1,var(X3),X6)
<=> X14 = X6 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_031) ).
fof(axiom_018,axiom,
! [X1,X2,X3] : proj3App(app(X1,X2,X3)) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_018) ).
fof(axiom_017,axiom,
! [X1,X2,X3] : proj2App(app(X1,X2,X3)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_017) ).
fof(axiom_016,axiom,
! [X1,X2,X3] : proj1App(app(X1,X2,X3)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_016) ).
fof(axiom_022,axiom,
! [X1,X2,X3,X4] : app(X1,X2,X3) != var(X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_022) ).
fof(axiom_021,axiom,
! [X1,X2,X3,X4] : app(X1,X2,X3) != lam(X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_021) ).
fof(axiom_026,axiom,
! [X6,X7,X8] : index(cons(X6,X7),suc(X8)) = index(X7,X8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_026) ).
fof(axiom_025,axiom,
! [X6,X7] : index(cons(X6,X7),zero) = just(X6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_025) ).
fof(axiom_005,axiom,
! [X1,X2] : proj2Arr(arr(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_005) ).
fof(axiom_004,axiom,
! [X1,X2] : proj1Arr(arr(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_004) ).
fof(axiom_002,axiom,
! [X1,X2] : tail(cons(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_002) ).
fof(axiom_001,axiom,
! [X1,X2] : head(cons(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_001) ).
fof(axiom_008,axiom,
! [X1,X2] : arr(X1,X2) != c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_008) ).
fof(axiom_007,axiom,
! [X1,X2] : arr(X1,X2) != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_007) ).
fof(axiom_006,axiom,
! [X1,X2] : arr(X1,X2) != a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_006) ).
fof(axiom_003,axiom,
! [X1,X2] : nil != cons(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_003) ).
fof(axiom_023,axiom,
! [X1,X2] : lam(X1) != var(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_023) ).
fof(axiom_024,axiom,
! [X5] : index(nil,X5) = nothing,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_024) ).
fof(axiom_020,axiom,
! [X1] : proj1Var(var(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_020) ).
fof(axiom_019,axiom,
! [X1] : proj1Lam(lam(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_019) ).
fof(axiom_014,axiom,
! [X1] : proj1Just(just(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_014) ).
fof(axiom_012,axiom,
! [X1] : proj1Suc(suc(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_012) ).
fof(axiom_015,axiom,
! [X1] : nothing != just(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_015) ).
fof(axiom_013,axiom,
! [X1] : zero != suc(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_013) ).
fof(axiom_011,axiom,
b != c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_011) ).
fof(axiom_010,axiom,
a != c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_010) ).
fof(axiom_009,axiom,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_009) ).
fof(i_0_32,negated_conjecture,
~ ? [X11] : tc(nil,X11,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(assume_negation,[status(cth)],[goal_032]) ).
fof(i_0_33,plain,
! [X1,X6,X11] :
( X6 != arr(proj1Arr(X6),proj2Arr(X6))
=> ~ tc(X1,lam(X11),X6) ),
inference(fof_simplification,[status(thm)],[axiom_028]) ).
fof(i_0_34,plain,
! [X1,X6,X3] :
( index(X1,X3) = nothing
=> ~ tc(X1,var(X3),X6) ),
inference(fof_simplification,[status(thm)],[axiom_030]) ).
fof(i_0_35,negated_conjecture,
! [X148] : ~ tc(nil,X148,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_32])]) ).
fof(i_0_36,plain,
! [X129,X130,X131,X132,X133] :
( ( tc(X129,X131,arr(X133,X130))
| ~ tc(X129,app(X131,X132,X133),X130) )
& ( tc(X129,X132,X133)
| ~ tc(X129,app(X131,X132,X133),X130) )
& ( ~ tc(X129,X131,arr(X133,X130))
| ~ tc(X129,X132,X133)
| tc(X129,app(X131,X132,X133),X130) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_027])])]) ).
fof(i_0_37,plain,
! [X137,X138,X139,X140] :
( ( ~ tc(X137,lam(X138),arr(X139,X140))
| tc(cons(X139,X137),X138,X140) )
& ( ~ tc(cons(X139,X137),X138,X140)
| tc(X137,lam(X138),arr(X139,X140)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_029])]) ).
fof(i_0_38,plain,
! [X144,X145,X146,X147] :
( ( ~ tc(X144,var(X146),X145)
| X147 = X145
| index(X144,X146) != just(X147) )
& ( X147 != X145
| tc(X144,var(X146),X145)
| index(X144,X146) != just(X147) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_031])])]) ).
fof(i_0_39,plain,
! [X134,X135,X136] :
( X135 = arr(proj1Arr(X135),proj2Arr(X135))
| ~ tc(X134,lam(X136),X135) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_33])]) ).
fof(i_0_40,plain,
! [X141,X142,X143] :
( index(X141,X143) != nothing
| ~ tc(X141,var(X143),X142) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_34])]) ).
fof(i_0_41,plain,
! [X108,X109,X110] : proj3App(app(X108,X109,X110)) = X110,
inference(variable_rename,[status(thm)],[axiom_018]) ).
fof(i_0_42,plain,
! [X105,X106,X107] : proj2App(app(X105,X106,X107)) = X106,
inference(variable_rename,[status(thm)],[axiom_017]) ).
fof(i_0_43,plain,
! [X102,X103,X104] : proj1App(app(X102,X103,X104)) = X102,
inference(variable_rename,[status(thm)],[axiom_016]) ).
fof(i_0_44,plain,
! [X117,X118,X119,X120] : app(X117,X118,X119) != var(X120),
inference(variable_rename,[status(thm)],[axiom_022]) ).
fof(i_0_45,plain,
! [X113,X114,X115,X116] : app(X113,X114,X115) != lam(X116),
inference(variable_rename,[status(thm)],[axiom_021]) ).
fof(i_0_46,plain,
! [X126,X127,X128] : index(cons(X126,X127),suc(X128)) = index(X127,X128),
inference(variable_rename,[status(thm)],[axiom_026]) ).
fof(i_0_47,plain,
! [X124,X125] : index(cons(X124,X125),zero) = just(X124),
inference(variable_rename,[status(thm)],[axiom_025]) ).
fof(i_0_48,plain,
! [X90,X91] : proj2Arr(arr(X90,X91)) = X91,
inference(variable_rename,[status(thm)],[axiom_005]) ).
fof(i_0_49,plain,
! [X88,X89] : proj1Arr(arr(X88,X89)) = X88,
inference(variable_rename,[status(thm)],[axiom_004]) ).
fof(i_0_50,plain,
! [X84,X85] : tail(cons(X84,X85)) = X85,
inference(variable_rename,[status(thm)],[axiom_002]) ).
fof(i_0_51,plain,
! [X82,X83] : head(cons(X82,X83)) = X82,
inference(variable_rename,[status(thm)],[axiom_001]) ).
fof(i_0_52,plain,
! [X96,X97] : arr(X96,X97) != c,
inference(variable_rename,[status(thm)],[axiom_008]) ).
fof(i_0_53,plain,
! [X94,X95] : arr(X94,X95) != b,
inference(variable_rename,[status(thm)],[axiom_007]) ).
fof(i_0_54,plain,
! [X92,X93] : arr(X92,X93) != a,
inference(variable_rename,[status(thm)],[axiom_006]) ).
fof(i_0_55,plain,
! [X86,X87] : nil != cons(X86,X87),
inference(variable_rename,[status(thm)],[axiom_003]) ).
fof(i_0_56,plain,
! [X121,X122] : lam(X121) != var(X122),
inference(variable_rename,[status(thm)],[axiom_023]) ).
fof(i_0_57,plain,
! [X123] : index(nil,X123) = nothing,
inference(variable_rename,[status(thm)],[axiom_024]) ).
fof(i_0_58,plain,
! [X112] : proj1Var(var(X112)) = X112,
inference(variable_rename,[status(thm)],[axiom_020]) ).
fof(i_0_59,plain,
! [X111] : proj1Lam(lam(X111)) = X111,
inference(variable_rename,[status(thm)],[axiom_019]) ).
fof(i_0_60,plain,
! [X100] : proj1Just(just(X100)) = X100,
inference(variable_rename,[status(thm)],[axiom_014]) ).
fof(i_0_61,plain,
! [X98] : proj1Suc(suc(X98)) = X98,
inference(variable_rename,[status(thm)],[axiom_012]) ).
fof(i_0_62,plain,
! [X101] : nothing != just(X101),
inference(variable_rename,[status(thm)],[axiom_015]) ).
fof(i_0_63,plain,
! [X99] : zero != suc(X99),
inference(variable_rename,[status(thm)],[axiom_013]) ).
cnf(i_0_64,negated_conjecture,
~ tc(nil,X1,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_65,plain,
( tc(X1,app(X2,X5,X3),X4)
| ~ tc(X1,X2,arr(X3,X4))
| ~ tc(X1,X5,X3) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_66,plain,
( tc(X1,X2,arr(X3,X4))
| ~ tc(X1,app(X2,X5,X3),X4) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_67,plain,
( tc(X1,X2,X3)
| ~ tc(X1,app(X4,X2,X3),X5) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_68,plain,
( tc(cons(X3,X1),X2,X4)
| ~ tc(X1,lam(X2),arr(X3,X4)) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_69,plain,
( tc(X2,lam(X3),arr(X1,X4))
| ~ tc(cons(X1,X2),X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_70,plain,
( X4 = X3
| ~ tc(X1,var(X2),X3)
| index(X1,X2) != just(X4) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_71,plain,
( X1 = arr(proj1Arr(X1),proj2Arr(X1))
| ~ tc(X2,lam(X3),X1) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_72,plain,
( index(X1,X2) != nothing
| ~ tc(X1,var(X2),X3) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_73,plain,
proj3App(app(X1,X2,X3)) = X3,
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_74,plain,
proj2App(app(X1,X2,X3)) = X2,
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_75,plain,
proj1App(app(X1,X2,X3)) = X1,
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_76,plain,
( tc(X3,var(X4),X2)
| X1 != X2
| index(X3,X4) != just(X1) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_77,plain,
app(X1,X2,X3) != var(X4),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_78,plain,
app(X1,X2,X3) != lam(X4),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_79,plain,
index(cons(X1,X2),suc(X3)) = index(X2,X3),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_80,plain,
index(cons(X1,X2),zero) = just(X1),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_81,plain,
proj2Arr(arr(X1,X2)) = X2,
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_82,plain,
proj1Arr(arr(X1,X2)) = X1,
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_83,plain,
tail(cons(X1,X2)) = X2,
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_84,plain,
head(cons(X1,X2)) = X1,
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_85,plain,
arr(X1,X2) != c,
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_86,plain,
arr(X1,X2) != b,
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_87,plain,
arr(X1,X2) != a,
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_88,plain,
nil != cons(X1,X2),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_89,plain,
lam(X1) != var(X2),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_90,plain,
index(nil,X1) = nothing,
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_91,plain,
proj1Var(var(X1)) = X1,
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_92,plain,
proj1Lam(lam(X1)) = X1,
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_93,plain,
proj1Just(just(X1)) = X1,
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_94,plain,
proj1Suc(suc(X1)) = X1,
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_95,plain,
nothing != just(X1),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_96,plain,
zero != suc(X1),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_97,plain,
b != c,
inference(split_conjunct,[status(thm)],[axiom_011]),
[final] ).
cnf(i_0_98,plain,
a != c,
inference(split_conjunct,[status(thm)],[axiom_010]),
[final] ).
cnf(i_0_99,plain,
a != b,
inference(split_conjunct,[status(thm)],[axiom_009]),
[final] ).
cnf(i_0_100,axiom,
X1 = X1 ).
cnf(i_0_101,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_102,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_103,axiom,
( X1 != X2
| arr(X1,X3) = arr(X2,X3) ) ).
cnf(i_0_104,axiom,
( X1 != X2
| arr(X3,X1) = arr(X3,X2) ) ).
cnf(i_0_105,axiom,
( X1 != X2
| proj3App(X1) = proj3App(X2) ) ).
cnf(i_0_106,axiom,
( X1 != X2
| proj2App(X1) = proj2App(X2) ) ).
cnf(i_0_107,axiom,
( X1 != X2
| proj1App(X1) = proj1App(X2) ) ).
cnf(i_0_108,axiom,
( X1 != X2
| suc(X1) = suc(X2) ) ).
cnf(i_0_109,axiom,
( X1 != X2
| tail(X1) = tail(X2) ) ).
cnf(i_0_110,axiom,
( X1 != X2
| head(X1) = head(X2) ) ).
cnf(i_0_111,axiom,
( X1 != X2
| proj1Var(X1) = proj1Var(X2) ) ).
cnf(i_0_112,axiom,
( X1 != X2
| proj1Lam(X1) = proj1Lam(X2) ) ).
cnf(i_0_113,axiom,
( X1 != X2
| proj1Just(X1) = proj1Just(X2) ) ).
cnf(i_0_114,axiom,
( X1 != X2
| proj1Suc(X1) = proj1Suc(X2) ) ).
cnf(i_0_115,axiom,
( X1 != X2
| app(X1,X3,X4) = app(X2,X3,X4) ) ).
cnf(i_0_116,axiom,
( X1 != X2
| app(X3,X1,X4) = app(X3,X2,X4) ) ).
cnf(i_0_117,axiom,
( X1 != X2
| app(X3,X4,X1) = app(X3,X4,X2) ) ).
cnf(i_0_118,axiom,
( X1 != X2
| cons(X1,X3) = cons(X2,X3) ) ).
cnf(i_0_119,axiom,
( X1 != X2
| cons(X3,X1) = cons(X3,X2) ) ).
cnf(i_0_120,axiom,
( X1 != X2
| lam(X1) = lam(X2) ) ).
cnf(i_0_121,axiom,
( X1 != X2
| var(X1) = var(X2) ) ).
cnf(i_0_122,axiom,
( X1 != X2
| index(X1,X3) = index(X2,X3) ) ).
cnf(i_0_123,axiom,
( X1 != X2
| index(X3,X1) = index(X3,X2) ) ).
cnf(i_0_124,axiom,
( X1 != X2
| just(X1) = just(X2) ) ).
cnf(i_0_125,axiom,
( X1 != X2
| proj1Arr(X1) = proj1Arr(X2) ) ).
cnf(i_0_126,axiom,
( X1 != X2
| proj2Arr(X1) = proj2Arr(X2) ) ).
cnf(i_0_127,axiom,
( X1 != X2
| ~ tc(X1,X3,X4)
| tc(X2,X3,X4) ) ).
cnf(i_0_128,axiom,
( X1 != X2
| ~ tc(X3,X1,X4)
| tc(X3,X2,X4) ) ).
cnf(i_0_129,axiom,
( X1 != X2
| ~ tc(X3,X4,X1)
| tc(X3,X4,X2) ) ).
cnf(i_0_667,plain,
~ tc(proj1Suc(suc(nil)),proj1Var(var(var(X1))),X2),
inference(scs_inference,[],[i_0_140,i_0_94,i_0_127]) ).
cnf(i_0_691,plain,
~ tc(proj2App(app(X1,nil,X2)),proj1Lam(lam(var(X3))),X4),
inference(scs_inference,[],[i_0_160,i_0_74,i_0_127]) ).
cnf(i_0_741,plain,
~ tc(proj1Var(var(nil)),proj1Var(var(var(X1))),X2),
inference(scs_inference,[],[i_0_140,i_0_91,i_0_127]) ).
cnf(i_0_792,plain,
proj3App(app(X1,X2,index(nil,X3))) = proj3App(app(X4,X5,nothing)),
inference(scs_inference,[],[i_0_73,i_0_791,i_0_102]) ).
cnf(i_0_794,plain,
proj3App(app(X1,X2,nothing)) = proj3App(app(X3,X4,index(nil,X5))),
inference(scs_inference,[],[i_0_73,i_0_791,i_0_102,i_0_101]) ).
cnf(i_0_836,plain,
proj3App(app(X1,X2,X3)) = proj1Lam(lam(X3)),
inference(scs_inference,[],[i_0_73,i_0_152,i_0_102]) ).
cnf(i_0_837,plain,
X1 = proj1Lam(lam(X1)),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_838,plain,
proj1Lam(lam(X1)) = proj3App(app(X2,X3,X1)),
inference(scs_inference,[],[i_0_73,i_0_152,i_0_102,i_0_101]) ).
cnf(i_0_903,plain,
tc(X1,lam(lam(var(zero))),arr(X2,arr(proj1Var(var(X3)),X3))),
inference(scs_inference,[],[i_0_150,i_0_69]) ).
cnf(i_0_904,plain,
tc(X1,lam(var(zero)),arr(proj1Var(var(X2)),X2)),
inference(rename_variables,[],[i_0_150]) ).
cnf(i_0_959,plain,
tc(cons(X1,X2),var(zero),proj1Var(var(X1))),
inference(rename_variables,[],[i_0_153]) ).
cnf(i_0_972,plain,
tc(cons(X1,X2),var(zero),proj1Var(var(X1))),
inference(rename_variables,[],[i_0_153]) ).
cnf(i_0_1032,plain,
proj2App(app(X1,nothing,X2)) = index(nil,X3),
inference(rename_variables,[],[i_0_876]) ).
cnf(i_0_1134,plain,
proj1Just(just(X1)) = proj3App(app(X2,X3,X1)),
inference(rename_variables,[],[i_0_841]) ).
cnf(i_0_1176,plain,
proj3App(app(X1,X2,X3)) = proj1Just(just(X3)),
inference(rename_variables,[],[i_0_839]) ).
cnf(i_0_1181,plain,
proj3App(app(X1,X2,X3)) = proj1Just(just(X3)),
inference(rename_variables,[],[i_0_839]) ).
cnf(i_0_1331,plain,
tail(cons(X1,X2)) = proj3App(app(X3,X4,X2)),
inference(rename_variables,[],[i_0_815]) ).
cnf(i_0_1374,plain,
proj3App(app(X1,X2,X3)) = head(cons(X3,X4)),
inference(rename_variables,[],[i_0_842]) ).
cnf(i_0_1376,plain,
X1 = proj1Lam(lam(X1)),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_1427,plain,
head(cons(X1,X2)) = proj3App(app(X3,X4,X1)),
inference(rename_variables,[],[i_0_844]) ).
cnf(i_0_1475,plain,
proj2App(app(X1,X2,X3)) = tail(cons(X4,X2)),
inference(rename_variables,[],[i_0_897]) ).
cnf(i_0_1526,plain,
tail(cons(X1,X2)) = proj2App(app(X3,X2,X4)),
inference(rename_variables,[],[i_0_899]) ).
cnf(i_0_1753,plain,
tc(X1,lam(var(zero)),arr(proj3App(app(X2,X3,X4)),X4)),
inference(rename_variables,[],[i_0_775]) ).
cnf(i_0_1806,plain,
~ tc(proj1Lam(lam(nil)),X1,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_1842,plain,
tc(cons(X1,X2),var(zero),tail(cons(X3,X1))),
inference(rename_variables,[],[i_0_399]) ).
cnf(i_0_1844,plain,
proj3App(app(X1,X2,X3)) = proj1Just(just(X3)),
inference(rename_variables,[],[i_0_839]) ).
cnf(i_0_2347,plain,
proj3App(app(X1,X2,X3)) = tail(cons(X4,X3)),
inference(rename_variables,[],[i_0_813]) ).
cnf(i_0_2349,plain,
proj3App(app(X1,X2,index(nil,X3))) = proj2App(app(X4,nothing,X5)),
inference(rename_variables,[],[i_0_858]) ).
cnf(i_0_2464,plain,
X1 = proj1Lam(lam(X1)),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_2548,plain,
proj1Just(just(X1)) = proj3App(app(X2,X3,X1)),
inference(rename_variables,[],[i_0_841]) ).
cnf(i_0_2550,plain,
proj1Just(just(X1)) = proj3App(app(X2,X3,X1)),
inference(rename_variables,[],[i_0_841]) ).
cnf(i_0_176,plain,
tc(X1,lam(var(zero)),arr(X2,proj1Lam(lam(X2)))),
inference(scs_inference,[],[i_0_167,i_0_69]) ).
cnf(i_0_178,plain,
~ tc(proj1Just(just(nil)),app(X1,X2,arr(a,arr(b,c))),arr(b,arr(a,c))),
inference(scs_inference,[],[i_0_170,i_0_167,i_0_69,i_0_66]) ).
cnf(i_0_180,plain,
proj1Lam(lam(nothing)) = proj1Lam(lam(index(nil,X1))),
inference(scs_inference,[],[i_0_170,i_0_167,i_0_172,i_0_69,i_0_66,i_0_101]) ).
cnf(i_0_181,plain,
~ tc(proj1Suc(suc(nil)),X1,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(scs_inference,[],[i_0_64,i_0_170,i_0_167,i_0_172,i_0_94,i_0_69,i_0_66,i_0_101,i_0_127]) ).
cnf(i_0_183,plain,
proj1Suc(suc(nothing)) = proj1Lam(lam(index(nil,X1))),
inference(scs_inference,[],[i_0_64,i_0_170,i_0_167,i_0_172,i_0_166,i_0_94,i_0_182,i_0_69,i_0_66,i_0_101,i_0_127,i_0_102]) ).
cnf(i_0_185,plain,
~ tc(nil,proj1Suc(suc(var(X1))),X2),
inference(scs_inference,[],[i_0_64,i_0_170,i_0_167,i_0_172,i_0_166,i_0_94,i_0_182,i_0_184,i_0_132,i_0_69,i_0_66,i_0_101,i_0_127,i_0_102,i_0_128]) ).
cnf(i_0_699,plain,
~ tc(proj1Var(var(nil)),proj1Just(just(var(X1))),X2),
inference(scs_inference,[],[i_0_174,i_0_91,i_0_127]) ).
cnf(i_0_717,plain,
~ tc(proj1Arr(arr(nil,X1)),proj1Just(just(var(X2))),X3),
inference(scs_inference,[],[i_0_174,i_0_82,i_0_127]) ).
cnf(i_0_845,plain,
proj3App(app(X1,X2,nothing)) = proj1Lam(lam(index(nil,X3))),
inference(scs_inference,[],[i_0_73,i_0_166,i_0_102]) ).
cnf(i_0_847,plain,
proj1Lam(lam(index(nil,X1))) = proj3App(app(X2,X3,nothing)),
inference(scs_inference,[],[i_0_73,i_0_166,i_0_102,i_0_101]) ).
cnf(i_0_921,plain,
tc(X1,lam(lam(var(zero))),arr(X2,arr(X3,proj1Var(var(X3))))),
inference(scs_inference,[],[i_0_164,i_0_69]) ).
cnf(i_0_922,plain,
tc(X1,lam(var(zero)),arr(X2,proj1Var(var(X2)))),
inference(rename_variables,[],[i_0_164]) ).
cnf(i_0_1231,plain,
proj1Lam(lam(X1)) = proj3App(app(X2,X3,X1)),
inference(rename_variables,[],[i_0_838]) ).
cnf(i_0_1268,plain,
tc(cons(X1,X2),var(zero),proj1Lam(lam(X1))),
inference(rename_variables,[],[i_0_167]) ).
cnf(i_0_1511,plain,
tc(cons(X1,X2),var(zero),proj1Lam(lam(X1))),
inference(rename_variables,[],[i_0_167]) ).
cnf(i_0_1900,plain,
~ tc(proj1Just(just(nil)),X1,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(rename_variables,[],[i_0_170]) ).
cnf(i_0_2211,plain,
proj3App(app(X1,X2,index(nil,X3))) = proj3App(app(X4,X5,nothing)),
inference(rename_variables,[],[i_0_792]) ).
cnf(i_0_2310,plain,
~ tc(proj2App(app(X1,nil,X2)),app(X3,proj1Lam(lam(var(X4))),X5),X6),
inference(scs_inference,[],[i_0_691,i_0_67]) ).
cnf(i_0_187,plain,
~ tc(proj1Suc(suc(nil)),app(X1,X2,arr(a,arr(b,c))),arr(b,arr(a,c))),
inference(scs_inference,[],[i_0_181,i_0_66]) ).
cnf(i_0_189,plain,
proj1Lam(lam(index(nil,X1))) = proj1Suc(suc(nothing)),
inference(scs_inference,[],[i_0_181,i_0_183,i_0_66,i_0_101]) ).
cnf(i_0_190,plain,
~ tc(proj2Arr(arr(X1,nil)),X2,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(scs_inference,[],[i_0_64,i_0_181,i_0_183,i_0_81,i_0_66,i_0_101,i_0_127]) ).
cnf(i_0_192,plain,
proj2Arr(arr(X1,nothing)) = proj1Lam(lam(index(nil,X2))),
inference(scs_inference,[],[i_0_64,i_0_181,i_0_183,i_0_81,i_0_191,i_0_166,i_0_66,i_0_101,i_0_127,i_0_102]) ).
cnf(i_0_194,plain,
~ tc(nil,proj2Arr(arr(X1,var(X2))),X3),
inference(scs_inference,[],[i_0_64,i_0_181,i_0_183,i_0_81,i_0_191,i_0_193,i_0_166,i_0_132,i_0_66,i_0_101,i_0_127,i_0_102,i_0_128]) ).
cnf(i_0_695,plain,
~ tc(proj1App(app(nil,X1,X2)),proj1Suc(suc(var(X3))),X4),
inference(scs_inference,[],[i_0_185,i_0_75,i_0_127]) ).
cnf(i_0_1320,plain,
tc(X1,lam(var(zero)),arr(X2,proj1Lam(lam(X2)))),
inference(rename_variables,[],[i_0_176]) ).
cnf(i_0_1326,plain,
tc(X1,lam(var(zero)),arr(X2,proj1Lam(lam(X2)))),
inference(rename_variables,[],[i_0_176]) ).
cnf(i_0_1989,plain,
~ tc(proj1Suc(suc(nil)),X1,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(rename_variables,[],[i_0_181]) ).
cnf(i_0_2629,plain,
proj1Lam(lam(index(nil,X1))) = proj3App(app(X2,X3,nothing)),
inference(rename_variables,[],[i_0_847]) ).
cnf(i_0_196,plain,
~ tc(proj2Arr(arr(X1,nil)),app(X2,X3,arr(a,arr(b,c))),arr(b,arr(a,c))),
inference(scs_inference,[],[i_0_190,i_0_66]) ).
cnf(i_0_198,plain,
proj1Lam(lam(index(nil,X1))) = proj2Arr(arr(X2,nothing)),
inference(scs_inference,[],[i_0_190,i_0_192,i_0_66,i_0_101]) ).
cnf(i_0_199,plain,
~ tc(proj1Arr(arr(nil,X1)),X2,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(scs_inference,[],[i_0_64,i_0_190,i_0_192,i_0_82,i_0_66,i_0_101,i_0_127]) ).
cnf(i_0_201,plain,
proj2Arr(arr(X1,nothing)) = proj1Suc(suc(nothing)),
inference(scs_inference,[],[i_0_64,i_0_190,i_0_192,i_0_189,i_0_82,i_0_66,i_0_101,i_0_127,i_0_102]) ).
cnf(i_0_202,plain,
proj1Lam(lam(index(nil,X1))) = proj1Suc(suc(nothing)),
inference(rename_variables,[],[i_0_189]) ).
cnf(i_0_203,plain,
~ tc(nil,proj1Arr(arr(var(X1),X2)),X3),
inference(scs_inference,[],[i_0_64,i_0_190,i_0_192,i_0_189,i_0_82,i_0_200,i_0_132,i_0_66,i_0_101,i_0_127,i_0_102,i_0_128]) ).
cnf(i_0_288,plain,
proj1Lam(lam(index(nil,X1))) = proj1Suc(suc(nothing)),
inference(rename_variables,[],[i_0_189]) ).
cnf(i_0_703,plain,
~ tc(proj1Lam(lam(nil)),proj2Arr(arr(X1,var(X2))),X3),
inference(scs_inference,[],[i_0_194,i_0_92,i_0_127]) ).
cnf(i_0_1361,plain,
~ tc(proj2Arr(arr(X1,nil)),X2,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(rename_variables,[],[i_0_190]) ).
cnf(i_0_2350,plain,
~ tc(proj1App(app(nil,X1,X2)),app(X3,proj1Suc(suc(var(X4))),X5),X6),
inference(scs_inference,[],[i_0_695,i_0_67]) ).
cnf(i_0_205,plain,
~ tc(proj1Arr(arr(nil,X1)),app(X2,X3,arr(a,arr(b,c))),arr(b,arr(a,c))),
inference(scs_inference,[],[i_0_199,i_0_66]) ).
cnf(i_0_207,plain,
proj1Suc(suc(nothing)) = proj2Arr(arr(X1,nothing)),
inference(scs_inference,[],[i_0_199,i_0_201,i_0_66,i_0_101]) ).
cnf(i_0_208,plain,
~ tc(tail(cons(X1,nil)),X2,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(scs_inference,[],[i_0_64,i_0_199,i_0_201,i_0_83,i_0_66,i_0_101,i_0_127]) ).
cnf(i_0_210,plain,
proj1Lam(lam(nothing)) = proj2Arr(arr(X1,nothing)),
inference(scs_inference,[],[i_0_64,i_0_199,i_0_198,i_0_180,i_0_201,i_0_83,i_0_66,i_0_101,i_0_127,i_0_102]) ).
cnf(i_0_211,plain,
proj1Lam(lam(index(nil,X1))) = proj2Arr(arr(X2,nothing)),
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_212,plain,
~ tc(nil,tail(cons(X1,var(X2))),X3),
inference(scs_inference,[],[i_0_64,i_0_199,i_0_198,i_0_180,i_0_201,i_0_83,i_0_209,i_0_132,i_0_66,i_0_101,i_0_127,i_0_102,i_0_128]) ).
cnf(i_0_234,plain,
proj1Lam(lam(index(nil,X1))) = proj2Arr(arr(X2,nothing)),
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_713,plain,
~ tc(proj2Arr(arr(X1,nil)),proj1Arr(arr(var(X2),X3)),X4),
inference(scs_inference,[],[i_0_203,i_0_81,i_0_127]) ).
cnf(i_0_745,plain,
~ tc(proj1Lam(lam(nil)),proj1Arr(arr(var(X1),X2)),X3),
inference(scs_inference,[],[i_0_203,i_0_92,i_0_127]) ).
cnf(i_0_1459,plain,
~ tc(proj1Arr(arr(nil,X1)),X2,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_214,plain,
~ tc(tail(cons(X1,nil)),app(X2,X3,arr(a,arr(b,c))),arr(b,arr(a,c))),
inference(scs_inference,[],[i_0_208,i_0_66]) ).
cnf(i_0_216,plain,
proj2Arr(arr(X1,nothing)) = proj1Lam(lam(nothing)),
inference(scs_inference,[],[i_0_208,i_0_210,i_0_66,i_0_101]) ).
cnf(i_0_217,plain,
tc(cons(proj1Suc(suc(nothing)),X1),var(zero),proj2Arr(arr(X2,nothing))),
inference(scs_inference,[],[i_0_208,i_0_207,i_0_210,i_0_80,i_0_66,i_0_101,i_0_76]) ).
cnf(i_0_220,plain,
~ tc(head(cons(nil,X1)),X2,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(scs_inference,[],[i_0_64,i_0_208,i_0_207,i_0_210,i_0_84,i_0_80,i_0_66,i_0_101,i_0_76,i_0_127]) ).
cnf(i_0_222,plain,
head(cons(nothing,X1)) = proj1Lam(lam(index(nil,X2))),
inference(scs_inference,[],[i_0_64,i_0_208,i_0_207,i_0_210,i_0_84,i_0_221,i_0_166,i_0_80,i_0_66,i_0_101,i_0_76,i_0_127,i_0_102]) ).
cnf(i_0_224,plain,
~ tc(nil,head(cons(var(X1),X2)),X3),
inference(scs_inference,[],[i_0_64,i_0_208,i_0_207,i_0_210,i_0_84,i_0_221,i_0_223,i_0_166,i_0_80,i_0_132,i_0_66,i_0_101,i_0_76,i_0_127,i_0_102,i_0_128]) ).
cnf(i_0_226,plain,
tc(X1,lam(var(zero)),arr(proj1Suc(suc(nothing)),proj2Arr(arr(X2,nothing)))),
inference(scs_inference,[],[i_0_64,i_0_208,i_0_207,i_0_210,i_0_84,i_0_221,i_0_223,i_0_166,i_0_80,i_0_132,i_0_66,i_0_101,i_0_76,i_0_127,i_0_102,i_0_128,i_0_69]) ).
cnf(i_0_683,plain,
~ tc(head(cons(nil,X1)),tail(cons(X2,var(X3))),X4),
inference(scs_inference,[],[i_0_212,i_0_84,i_0_127]) ).
cnf(i_0_757,plain,
~ tc(proj1Arr(arr(nil,X1)),tail(cons(X2,var(X3))),X4),
inference(scs_inference,[],[i_0_212,i_0_82,i_0_127]) ).
cnf(i_0_1532,plain,
~ tc(tail(cons(X1,nil)),X2,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(rename_variables,[],[i_0_208]) ).
cnf(i_0_228,plain,
~ tc(head(cons(nil,X1)),app(X2,X3,arr(a,arr(b,c))),arr(b,arr(a,c))),
inference(scs_inference,[],[i_0_220,i_0_66]) ).
cnf(i_0_230,plain,
proj1Lam(lam(index(nil,X1))) = head(cons(nothing,X2)),
inference(scs_inference,[],[i_0_220,i_0_222,i_0_66,i_0_101]) ).
cnf(i_0_231,plain,
~ tc(proj3App(app(X1,X2,nil)),X3,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(scs_inference,[],[i_0_64,i_0_220,i_0_222,i_0_73,i_0_66,i_0_101,i_0_127]) ).
cnf(i_0_233,plain,
head(cons(nothing,X1)) = proj2Arr(arr(X2,nothing)),
inference(scs_inference,[],[i_0_64,i_0_220,i_0_222,i_0_73,i_0_198,i_0_66,i_0_101,i_0_127,i_0_102]) ).
cnf(i_0_235,plain,
~ tc(nil,proj3App(app(X1,X2,var(X3))),X4),
inference(scs_inference,[],[i_0_64,i_0_220,i_0_222,i_0_73,i_0_232,i_0_198,i_0_132,i_0_66,i_0_101,i_0_127,i_0_102,i_0_128]) ).
cnf(i_0_243,plain,
proj2Arr(arr(X1,nothing)) = proj1Lam(lam(nothing)),
inference(rename_variables,[],[i_0_216]) ).
cnf(i_0_558,plain,
tc(X1,lam(var(zero)),arr(proj1Suc(suc(nothing)),proj2Arr(arr(X2,nothing)))),
inference(rename_variables,[],[i_0_226]) ).
cnf(i_0_671,plain,
~ tc(proj2Arr(arr(X1,nil)),head(cons(var(X2),X3)),X4),
inference(scs_inference,[],[i_0_224,i_0_81,i_0_127]) ).
cnf(i_0_687,plain,
~ tc(proj3App(app(X1,X2,nil)),head(cons(var(X3),X4)),X5),
inference(scs_inference,[],[i_0_224,i_0_73,i_0_127]) ).
cnf(i_0_725,plain,
~ tc(head(cons(nil,X1)),head(cons(var(X2),X3)),X4),
inference(scs_inference,[],[i_0_224,i_0_84,i_0_127]) ).
cnf(i_0_1625,plain,
~ tc(head(cons(nil,X1)),X2,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(rename_variables,[],[i_0_220]) ).
cnf(i_0_237,plain,
~ tc(proj3App(app(X1,X2,nil)),app(X3,X4,arr(a,arr(b,c))),arr(b,arr(a,c))),
inference(scs_inference,[],[i_0_231,i_0_66]) ).
cnf(i_0_239,plain,
proj2Arr(arr(X1,nothing)) = head(cons(nothing,X2)),
inference(scs_inference,[],[i_0_231,i_0_233,i_0_66,i_0_101]) ).
cnf(i_0_240,plain,
~ tc(proj2App(app(X1,nil,X2)),X3,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(scs_inference,[],[i_0_64,i_0_231,i_0_233,i_0_74,i_0_66,i_0_101,i_0_127]) ).
cnf(i_0_242,plain,
head(cons(nothing,X1)) = proj1Lam(lam(nothing)),
inference(scs_inference,[],[i_0_64,i_0_231,i_0_233,i_0_216,i_0_74,i_0_66,i_0_101,i_0_127,i_0_102]) ).
cnf(i_0_244,plain,
~ tc(nil,proj2App(app(X1,var(X2),X3)),X4),
inference(scs_inference,[],[i_0_64,i_0_231,i_0_233,i_0_216,i_0_74,i_0_241,i_0_132,i_0_66,i_0_101,i_0_127,i_0_102,i_0_128]) ).
cnf(i_0_675,plain,
~ tc(proj1Arr(arr(nil,X1)),proj3App(app(X2,X3,var(X4))),X5),
inference(scs_inference,[],[i_0_235,i_0_82,i_0_127]) ).
cnf(i_0_721,plain,
~ tc(tail(cons(X1,nil)),proj3App(app(X2,X3,var(X4))),X5),
inference(scs_inference,[],[i_0_235,i_0_83,i_0_127]) ).
cnf(i_0_761,plain,
~ tc(head(cons(nil,X1)),proj3App(app(X2,X3,var(X4))),X5),
inference(scs_inference,[],[i_0_235,i_0_84,i_0_127]) ).
cnf(i_0_1065,plain,
~ tc(proj3App(app(X1,X2,nil)),X3,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(rename_variables,[],[i_0_231]) ).
cnf(i_0_2219,plain,
~ tc(proj3App(app(X1,X2,nil)),app(X3,head(cons(var(X4),X5)),X6),X7),
inference(scs_inference,[],[i_0_687,i_0_67]) ).
cnf(i_0_246,plain,
~ tc(proj2App(app(X1,nil,X2)),app(X3,X4,arr(a,arr(b,c))),arr(b,arr(a,c))),
inference(scs_inference,[],[i_0_240,i_0_66]) ).
cnf(i_0_248,plain,
proj1Lam(lam(nothing)) = head(cons(nothing,X1)),
inference(scs_inference,[],[i_0_240,i_0_242,i_0_66,i_0_101]) ).
cnf(i_0_249,plain,
~ tc(proj1App(app(nil,X1,X2)),X3,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(scs_inference,[],[i_0_64,i_0_240,i_0_242,i_0_75,i_0_66,i_0_101,i_0_127]) ).
cnf(i_0_251,plain,
~ tc(nil,proj1App(app(var(X1),X2,X3)),X4),
inference(scs_inference,[],[i_0_64,i_0_240,i_0_242,i_0_75,i_0_250,i_0_132,i_0_66,i_0_101,i_0_127,i_0_128]) ).
cnf(i_0_253,plain,
index(cons(X1,nil),suc(X2)) = nothing,
inference(scs_inference,[],[i_0_64,i_0_240,i_0_242,i_0_79,i_0_75,i_0_250,i_0_90,i_0_132,i_0_66,i_0_101,i_0_127,i_0_128,i_0_102]) ).
cnf(i_0_256,plain,
~ tc(cons(X1,nil),var(suc(X2)),X3),
inference(scs_inference,[],[i_0_64,i_0_240,i_0_242,i_0_79,i_0_75,i_0_250,i_0_90,i_0_132,i_0_66,i_0_101,i_0_127,i_0_128,i_0_102,i_0_72]) ).
cnf(i_0_266,plain,
proj2Arr(arr(X1,nothing)) = head(cons(nothing,X2)),
inference(rename_variables,[],[i_0_239]) ).
cnf(i_0_679,plain,
~ tc(tail(cons(X1,nil)),proj2App(app(X2,var(X3),X4)),X5),
inference(scs_inference,[],[i_0_244,i_0_83,i_0_127]) ).
cnf(i_0_729,plain,
~ tc(proj3App(app(X1,X2,nil)),proj2App(app(X3,var(X4),X5)),X6),
inference(scs_inference,[],[i_0_244,i_0_73,i_0_127]) ).
cnf(i_0_755,plain,
~ tc(proj2Arr(arr(X1,nil)),proj2App(app(X2,var(X3),X4)),X5),
inference(scs_inference,[],[i_0_244,i_0_81,i_0_127]) ).
cnf(i_0_1164,plain,
~ tc(proj2App(app(X1,nil,X2)),X3,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(rename_variables,[],[i_0_240]) ).
cnf(i_0_258,plain,
~ tc(proj1App(app(nil,X1,X2)),app(X3,X4,arr(a,arr(b,c))),arr(b,arr(a,c))),
inference(scs_inference,[],[i_0_249,i_0_66]) ).
cnf(i_0_260,plain,
nothing = index(cons(X1,nil),suc(X2)),
inference(scs_inference,[],[i_0_249,i_0_253,i_0_66,i_0_101]) ).
cnf(i_0_261,plain,
~ tc(proj1Just(just(nil)),proj1Var(var(var(X1))),X2),
inference(scs_inference,[],[i_0_249,i_0_140,i_0_253,i_0_93,i_0_66,i_0_101,i_0_127]) ).
cnf(i_0_263,plain,
~ tc(proj1Just(just(nil)),var(X1),X2),
inference(scs_inference,[],[i_0_249,i_0_140,i_0_253,i_0_134,i_0_93,i_0_66,i_0_101,i_0_127,i_0_128]) ).
cnf(i_0_265,plain,
proj1Suc(suc(nothing)) = head(cons(nothing,X1)),
inference(scs_inference,[],[i_0_249,i_0_140,i_0_239,i_0_253,i_0_134,i_0_207,i_0_93,i_0_66,i_0_101,i_0_127,i_0_128,i_0_102]) ).
cnf(i_0_291,plain,
~ tc(cons(X1,nil),app(var(suc(X2)),X3,X4),X5),
inference(scs_inference,[],[i_0_256,i_0_66]) ).
cnf(i_0_292,plain,
~ tc(cons(X1,nil),var(suc(X2)),X3),
inference(rename_variables,[],[i_0_256]) ).
cnf(i_0_709,plain,
~ tc(proj1Suc(suc(nil)),proj1App(app(var(X1),X2,X3)),X4),
inference(scs_inference,[],[i_0_251,i_0_94,i_0_127]) ).
cnf(i_0_733,plain,
~ tc(proj2App(app(X1,nil,X2)),proj1App(app(var(X3),X4,X5)),X6),
inference(scs_inference,[],[i_0_251,i_0_74,i_0_127]) ).
cnf(i_0_737,plain,
~ tc(proj1App(app(cons(X1,nil),X2,X3)),var(suc(X4)),X5),
inference(scs_inference,[],[i_0_256,i_0_75,i_0_127]) ).
cnf(i_0_751,plain,
~ tc(proj1Suc(suc(cons(X1,nil))),var(suc(X2)),X3),
inference(scs_inference,[],[i_0_256,i_0_94,i_0_127]) ).
cnf(i_0_759,plain,
~ tc(tail(cons(X1,cons(X2,nil))),var(suc(X3)),X4),
inference(scs_inference,[],[i_0_256,i_0_83,i_0_127]) ).
cnf(i_0_763,plain,
~ tc(proj3App(app(X1,X2,cons(X3,nil))),var(suc(X4)),X5),
inference(scs_inference,[],[i_0_256,i_0_73,i_0_127]) ).
cnf(i_0_765,plain,
~ tc(proj2App(app(X1,cons(X2,nil),X3)),var(suc(X4)),X5),
inference(scs_inference,[],[i_0_256,i_0_74,i_0_127]) ).
cnf(i_0_1261,plain,
~ tc(proj1App(app(nil,X1,X2)),X3,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))),
inference(rename_variables,[],[i_0_249]) ).
cnf(i_0_2392,plain,
~ tc(proj3App(app(X1,X2,nil)),app(X3,proj2App(app(X4,var(X5),X6)),X7),X8),
inference(scs_inference,[],[i_0_729,i_0_67]) ).
cnf(i_0_267,plain,
~ tc(proj1Just(just(nil)),app(var(X1),X2,X3),X4),
inference(scs_inference,[],[i_0_263,i_0_66]) ).
cnf(i_0_268,plain,
~ tc(proj1Just(just(nil)),var(X1),X2),
inference(rename_variables,[],[i_0_263]) ).
cnf(i_0_270,plain,
head(cons(nothing,X1)) = proj1Suc(suc(nothing)),
inference(scs_inference,[],[i_0_263,i_0_265,i_0_66,i_0_101]) ).
cnf(i_0_271,plain,
~ tc(proj1Suc(suc(nil)),proj1Lam(lam(var(X1))),X2),
inference(scs_inference,[],[i_0_263,i_0_160,i_0_265,i_0_94,i_0_66,i_0_101,i_0_127]) ).
cnf(i_0_833,plain,
proj3App(app(X1,X2,nothing)) = index(cons(X3,nil),suc(X4)),
inference(scs_inference,[],[i_0_73,i_0_260,i_0_102]) ).
cnf(i_0_835,plain,
index(cons(X1,nil),suc(X2)) = proj3App(app(X3,X4,nothing)),
inference(scs_inference,[],[i_0_73,i_0_260,i_0_102,i_0_101]) ).
cnf(i_0_906,plain,
~ tc(proj1App(app(cons(X1,nil),X2,X3)),app(var(suc(X4)),X5,X6),X7),
inference(scs_inference,[],[i_0_737,i_0_150,i_0_69,i_0_66]) ).
cnf(i_0_907,plain,
~ tc(proj1App(app(cons(X1,nil),X2,X3)),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_737]) ).
cnf(i_0_909,plain,
~ tc(nil,app(X1,X2,arr(a,arr(b,c))),proj2App(app(X3,arr(b,arr(a,c)),X4))),
inference(scs_inference,[],[i_0_74,i_0_737,i_0_150,i_0_130,i_0_69,i_0_66,i_0_129]) ).
cnf(i_0_924,plain,
~ tc(proj3App(app(X1,X2,cons(X3,nil))),app(var(suc(X4)),X5,X6),X7),
inference(scs_inference,[],[i_0_763,i_0_164,i_0_69,i_0_66]) ).
cnf(i_0_925,plain,
~ tc(proj3App(app(X1,X2,cons(X3,nil))),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_763]) ).
cnf(i_0_977,plain,
~ tc(proj2App(app(X1,cons(X2,nil),X3)),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_765]) ).
cnf(i_0_1025,plain,
~ tc(tail(cons(X1,cons(X2,nil))),var(suc(X3)),X4),
inference(rename_variables,[],[i_0_759]) ).
cnf(i_0_1088,plain,
~ tc(proj1Suc(suc(cons(X1,nil))),app(X2,var(suc(X3)),X4),X5),
inference(scs_inference,[],[i_0_751,i_0_67]) ).
cnf(i_0_1129,plain,
~ tc(proj1Suc(suc(cons(X1,nil))),var(suc(X2)),X3),
inference(rename_variables,[],[i_0_751]) ).
cnf(i_0_1178,plain,
~ tc(proj1App(app(cons(X1,nil),X2,X3)),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_737]) ).
cnf(i_0_1225,plain,
~ tc(proj3App(app(X1,X2,cons(X3,nil))),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_763]) ).
cnf(i_0_1274,plain,
~ tc(proj2App(app(X1,cons(X2,nil),X3)),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_765]) ).
cnf(i_0_1323,plain,
~ tc(tail(cons(X1,cons(X2,nil))),var(suc(X3)),X4),
inference(rename_variables,[],[i_0_759]) ).
cnf(i_0_1470,plain,
~ tc(proj1App(app(cons(X1,nil),X2,X3)),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_737]) ).
cnf(i_0_1518,plain,
~ tc(proj3App(app(X1,X2,cons(X3,nil))),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_763]) ).
cnf(i_0_1567,plain,
~ tc(proj2App(app(X1,cons(X2,nil),X3)),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_765]) ).
cnf(i_0_1613,plain,
~ tc(tail(cons(X1,cons(X2,nil))),var(suc(X3)),X4),
inference(rename_variables,[],[i_0_759]) ).
cnf(i_0_1705,plain,
~ tc(proj1Suc(suc(cons(X1,nil))),var(suc(X2)),X3),
inference(rename_variables,[],[i_0_751]) ).
cnf(i_0_1794,plain,
~ tc(proj1App(app(cons(X1,nil),X2,X3)),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_737]) ).
cnf(i_0_1837,plain,
~ tc(proj3App(app(X1,X2,cons(X3,nil))),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_763]) ).
cnf(i_0_1888,plain,
~ tc(proj2App(app(X1,cons(X2,nil),X3)),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_765]) ).
cnf(i_0_1932,plain,
~ tc(tail(cons(X1,cons(X2,nil))),var(suc(X3)),X4),
inference(rename_variables,[],[i_0_759]) ).
cnf(i_0_2020,plain,
~ tc(proj1Suc(suc(cons(X1,nil))),var(suc(X2)),X3),
inference(rename_variables,[],[i_0_751]) ).
cnf(i_0_2168,plain,
~ tc(proj1App(app(cons(X1,nil),X2,X3)),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_737]) ).
cnf(i_0_2208,plain,
~ tc(proj3App(app(X1,X2,cons(X3,nil))),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_763]) ).
cnf(i_0_2250,plain,
~ tc(proj2App(app(X1,cons(X2,nil),X3)),var(suc(X4)),X5),
inference(rename_variables,[],[i_0_765]) ).
cnf(i_0_2292,plain,
~ tc(tail(cons(X1,cons(X2,nil))),var(suc(X3)),X4),
inference(rename_variables,[],[i_0_759]) ).
cnf(i_0_2382,plain,
~ tc(proj1Suc(suc(cons(X1,nil))),var(suc(X2)),X3),
inference(rename_variables,[],[i_0_751]) ).
cnf(i_0_2473,plain,
~ tc(proj2App(app(X1,nil,X2)),app(X3,proj1App(app(var(X4),X5,X6)),X7),X8),
inference(scs_inference,[],[i_0_733,i_0_67]) ).
cnf(i_0_273,plain,
~ tc(proj1Just(just(nil)),proj1Suc(suc(var(X1))),X2),
inference(scs_inference,[],[i_0_263,i_0_268,i_0_160,i_0_265,i_0_94,i_0_272,i_0_66,i_0_101,i_0_127,i_0_128]) ).
cnf(i_0_275,plain,
index(cons(X1,nil),suc(X2)) = index(cons(X3,nil),suc(X4)),
inference(scs_inference,[],[i_0_263,i_0_268,i_0_160,i_0_265,i_0_260,i_0_253,i_0_94,i_0_272,i_0_66,i_0_101,i_0_127,i_0_128,i_0_102]) ).
cnf(i_0_276,plain,
~ tc(proj1Just(just(nil)),app(app(var(X1),X2,X3),X4,X5),X6),
inference(scs_inference,[],[i_0_267,i_0_66]) ).
cnf(i_0_277,plain,
~ tc(proj1Just(just(nil)),app(var(X1),X2,X3),X4),
inference(rename_variables,[],[i_0_267]) ).
cnf(i_0_279,plain,
index(X1,X2) = index(cons(X3,X1),suc(X2)),
inference(scs_inference,[],[i_0_267,i_0_79,i_0_66,i_0_101]) ).
cnf(i_0_344,plain,
head(cons(nothing,X1)) = proj1Suc(suc(nothing)),
inference(rename_variables,[],[i_0_270]) ).
cnf(i_0_425,plain,
head(cons(nothing,X1)) = proj1Suc(suc(nothing)),
inference(rename_variables,[],[i_0_270]) ).
cnf(i_0_927,plain,
~ tc(proj3App(app(X1,X2,cons(X3,nil))),proj2App(app(X4,var(suc(X5)),X6)),X7),
inference(scs_inference,[],[i_0_74,i_0_763,i_0_925,i_0_164,i_0_69,i_0_66,i_0_128]) ).
cnf(i_0_280,plain,
tc(cons(index(cons(X1,nil),suc(X2)),X3),var(zero),index(cons(X4,nil),suc(X5))),
inference(scs_inference,[],[i_0_267,i_0_275,i_0_79,i_0_80,i_0_66,i_0_101,i_0_76]) ).
cnf(i_0_283,plain,
~ tc(proj2Arr(arr(X1,nil)),proj1Just(just(var(X2))),X3),
inference(scs_inference,[],[i_0_267,i_0_174,i_0_275,i_0_79,i_0_81,i_0_80,i_0_66,i_0_101,i_0_76,i_0_127]) ).
cnf(i_0_285,plain,
~ tc(proj1Just(just(nil)),proj2Arr(arr(X1,var(X2))),X3),
inference(scs_inference,[],[i_0_267,i_0_174,i_0_263,i_0_275,i_0_79,i_0_81,i_0_284,i_0_80,i_0_66,i_0_101,i_0_76,i_0_127,i_0_128]) ).
cnf(i_0_287,plain,
proj1Lam(lam(nothing)) = proj1Suc(suc(nothing)),
inference(scs_inference,[],[i_0_267,i_0_174,i_0_263,i_0_275,i_0_189,i_0_180,i_0_79,i_0_81,i_0_284,i_0_80,i_0_66,i_0_101,i_0_76,i_0_127,i_0_128,i_0_102]) ).
cnf(i_0_289,plain,
tc(X1,lam(var(zero)),arr(index(cons(X2,nil),suc(X3)),index(cons(X4,nil),suc(X5)))),
inference(scs_inference,[],[i_0_267,i_0_174,i_0_263,i_0_275,i_0_189,i_0_180,i_0_79,i_0_81,i_0_284,i_0_80,i_0_66,i_0_101,i_0_76,i_0_127,i_0_128,i_0_102,i_0_69]) ).
cnf(i_0_303,plain,
index(X1,X2) = index(cons(X3,X1),suc(X2)),
inference(rename_variables,[],[i_0_279]) ).
cnf(i_0_1616,plain,
index(X1,X2) = index(cons(X3,X1),suc(X2)),
inference(rename_variables,[],[i_0_279]) ).
cnf(i_0_1846,plain,
index(X1,X2) = index(cons(X3,X1),suc(X2)),
inference(rename_variables,[],[i_0_279]) ).
cnf(i_0_294,plain,
proj1Suc(suc(nothing)) = proj1Lam(lam(nothing)),
inference(scs_inference,[],[i_0_256,i_0_287,i_0_66,i_0_101]) ).
cnf(i_0_295,plain,
tc(cons(index(X1,X2),X3),var(zero),index(cons(X4,X1),suc(X2))),
inference(scs_inference,[],[i_0_279,i_0_256,i_0_287,i_0_80,i_0_66,i_0_101,i_0_76]) ).
cnf(i_0_298,plain,
~ tc(proj1Arr(arr(nil,X1)),proj1Suc(suc(var(X2))),X3),
inference(scs_inference,[],[i_0_185,i_0_279,i_0_256,i_0_287,i_0_82,i_0_80,i_0_66,i_0_101,i_0_76,i_0_127]) ).
cnf(i_0_300,plain,
~ tc(proj1Just(just(nil)),proj1Arr(arr(var(X1),X2)),X3),
inference(scs_inference,[],[i_0_185,i_0_263,i_0_279,i_0_256,i_0_287,i_0_82,i_0_299,i_0_80,i_0_66,i_0_101,i_0_76,i_0_127,i_0_128]) ).
cnf(i_0_302,plain,
index(cons(X1,nil),suc(X2)) = index(cons(X3,cons(X4,nil)),suc(suc(X5))),
inference(scs_inference,[],[i_0_185,i_0_263,i_0_279,i_0_256,i_0_287,i_0_275,i_0_82,i_0_299,i_0_80,i_0_66,i_0_101,i_0_76,i_0_127,i_0_128,i_0_102]) ).
cnf(i_0_912,plain,
tc(X1,lam(var(zero)),arr(index(cons(X2,nil),suc(X3)),index(cons(X4,nil),suc(X5)))),
inference(rename_variables,[],[i_0_289]) ).
cnf(i_0_914,plain,
~ tc(proj1App(app(cons(X1,nil),X2,X3)),proj2App(app(X4,var(suc(X5)),X6)),X7),
inference(scs_inference,[],[i_0_74,i_0_910,i_0_737,i_0_907,i_0_150,i_0_289,i_0_280,i_0_130,i_0_69,i_0_66,i_0_129,i_0_65,i_0_128]) ).
cnf(i_0_304,plain,
tc(X1,lam(var(zero)),arr(index(X2,X3),index(cons(X4,X2),suc(X3)))),
inference(scs_inference,[],[i_0_295,i_0_69]) ).
cnf(i_0_306,plain,
~ tc(nil,app(var(X1),X2,X3),X4),
inference(scs_inference,[],[i_0_295,i_0_132,i_0_69,i_0_66]) ).
cnf(i_0_309,plain,
index(cons(X1,cons(X2,nil)),suc(suc(X3))) = index(cons(X4,nil),suc(X5)),
inference(scs_inference,[],[i_0_295,i_0_302,i_0_132,i_0_69,i_0_66,i_0_101]) ).
cnf(i_0_310,plain,
~ tc(tail(cons(X1,nil)),proj2Arr(arr(X2,var(X3))),X4),
inference(scs_inference,[],[i_0_295,i_0_194,i_0_302,i_0_83,i_0_132,i_0_69,i_0_66,i_0_101,i_0_127]) ).
cnf(i_0_312,plain,
~ tc(proj1Just(just(nil)),tail(cons(X1,var(X2))),X3),
inference(scs_inference,[],[i_0_295,i_0_194,i_0_263,i_0_302,i_0_83,i_0_311,i_0_132,i_0_69,i_0_66,i_0_101,i_0_127,i_0_128]) ).
cnf(i_0_314,plain,
nothing = index(cons(X1,cons(X2,nil)),suc(suc(X3))),
inference(scs_inference,[],[i_0_295,i_0_194,i_0_263,i_0_302,i_0_260,i_0_83,i_0_311,i_0_132,i_0_69,i_0_66,i_0_101,i_0_127,i_0_128,i_0_102]) ).
cnf(i_0_315,plain,
index(cons(X1,nil),suc(X2)) = index(cons(X3,cons(X4,nil)),suc(suc(X5))),
inference(rename_variables,[],[i_0_302]) ).
cnf(i_0_1265,plain,
tc(cons(index(X1,X2),X3),var(zero),index(cons(X4,X1),suc(X2))),
inference(rename_variables,[],[i_0_295]) ).
cnf(i_0_2338,plain,
tc(cons(index(X1,X2),X3),var(zero),index(cons(X4,X1),suc(X2))),
inference(rename_variables,[],[i_0_295]) ).
cnf(i_0_316,plain,
~ tc(nil,app(app(var(X1),X2,X3),X4,X5),X6),
inference(scs_inference,[],[i_0_306,i_0_66]) ).
cnf(i_0_317,plain,
~ tc(nil,app(var(X1),X2,X3),X4),
inference(rename_variables,[],[i_0_306]) ).
cnf(i_0_319,plain,
index(cons(X1,cons(X2,nil)),suc(suc(X3))) = nothing,
inference(scs_inference,[],[i_0_306,i_0_314,i_0_66,i_0_101]) ).
cnf(i_0_337,plain,
index(cons(X1,cons(X2,nil)),suc(suc(X3))) = index(cons(X4,nil),suc(X5)),
inference(rename_variables,[],[i_0_309]) ).
cnf(i_0_357,plain,
index(cons(X1,cons(X2,nil)),suc(suc(X3))) = index(cons(X4,nil),suc(X5)),
inference(rename_variables,[],[i_0_309]) ).
cnf(i_0_566,plain,
~ tc(tail(cons(X1,nil)),proj2Arr(arr(X2,var(X3))),X4),
inference(rename_variables,[],[i_0_310]) ).
cnf(i_0_830,plain,
proj3App(app(X1,X2,nothing)) = index(cons(X3,cons(X4,nil)),suc(suc(X5))),
inference(scs_inference,[],[i_0_73,i_0_314,i_0_102]) ).
cnf(i_0_832,plain,
index(cons(X1,cons(X2,nil)),suc(suc(X3))) = proj3App(app(X4,X5,nothing)),
inference(scs_inference,[],[i_0_73,i_0_314,i_0_102,i_0_101]) ).
cnf(i_0_1416,plain,
tc(X1,lam(var(zero)),arr(index(X2,X3),index(cons(X4,X2),suc(X3)))),
inference(rename_variables,[],[i_0_304]) ).
cnf(i_0_1422,plain,
tc(X1,lam(var(zero)),arr(index(X2,X3),index(cons(X4,X2),suc(X3)))),
inference(rename_variables,[],[i_0_304]) ).
cnf(i_0_320,plain,
~ tc(head(cons(nil,X1)),app(var(X2),X3,X4),X5),
inference(scs_inference,[],[i_0_306,i_0_317,i_0_314,i_0_84,i_0_66,i_0_101,i_0_127]) ).
cnf(i_0_322,plain,
~ tc(proj1Just(just(nil)),head(cons(var(X1),X2)),X3),
inference(scs_inference,[],[i_0_306,i_0_317,i_0_263,i_0_314,i_0_84,i_0_321,i_0_66,i_0_101,i_0_127,i_0_128]) ).
cnf(i_0_324,plain,
head(cons(nothing,X1)) = index(cons(X2,cons(X3,nil)),suc(suc(X4))),
inference(scs_inference,[],[i_0_306,i_0_317,i_0_263,i_0_314,i_0_84,i_0_321,i_0_323,i_0_66,i_0_101,i_0_127,i_0_128,i_0_102]) ).
cnf(i_0_326,plain,
~ tc(cons(X1,cons(X2,nil)),var(suc(suc(X3))),X4),
inference(scs_inference,[],[i_0_306,i_0_317,i_0_263,i_0_314,i_0_84,i_0_321,i_0_323,i_0_66,i_0_101,i_0_127,i_0_128,i_0_102,i_0_72]) ).
cnf(i_0_328,plain,
~ tc(head(cons(nil,X1)),app(app(var(X2),X3,X4),X5,X6),X7),
inference(scs_inference,[],[i_0_320,i_0_66]) ).
cnf(i_0_329,plain,
~ tc(head(cons(nil,X1)),app(var(X2),X3,X4),X5),
inference(rename_variables,[],[i_0_320]) ).
cnf(i_0_331,plain,
index(cons(X1,cons(X2,nil)),suc(suc(X3))) = head(cons(nothing,X4)),
inference(scs_inference,[],[i_0_320,i_0_324,i_0_66,i_0_101]) ).
cnf(i_0_332,plain,
~ tc(proj3App(app(X1,X2,nil)),proj1Arr(arr(var(X3),X4)),X5),
inference(scs_inference,[],[i_0_320,i_0_203,i_0_324,i_0_73,i_0_66,i_0_101,i_0_127]) ).
cnf(i_0_334,plain,
~ tc(proj1Just(just(nil)),proj3App(app(X1,X2,var(X3))),X4),
inference(scs_inference,[],[i_0_320,i_0_203,i_0_263,i_0_324,i_0_73,i_0_333,i_0_66,i_0_101,i_0_127,i_0_128]) ).
cnf(i_0_336,plain,
head(cons(nothing,X1)) = index(cons(X2,nil),suc(X3)),
inference(scs_inference,[],[i_0_320,i_0_203,i_0_263,i_0_309,i_0_324,i_0_73,i_0_333,i_0_66,i_0_101,i_0_127,i_0_128,i_0_102]) ).
cnf(i_0_1419,plain,
~ tc(cons(X1,cons(X2,nil)),var(suc(suc(X3))),X4),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_1749,plain,
~ tc(cons(X1,cons(X2,nil)),var(suc(suc(X3))),X4),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_2075,plain,
~ tc(cons(X1,cons(X2,nil)),var(suc(suc(X3))),X4),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_2420,plain,
~ tc(cons(X1,cons(X2,nil)),var(suc(suc(X3))),X4),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_338,plain,
index(cons(X1,nil),suc(X2)) = head(cons(nothing,X3)),
inference(scs_inference,[],[i_0_336,i_0_101]) ).
cnf(i_0_339,plain,
~ tc(proj2App(app(X1,nil,X2)),tail(cons(X3,var(X4))),X5),
inference(scs_inference,[],[i_0_212,i_0_336,i_0_74,i_0_101,i_0_127]) ).
cnf(i_0_341,plain,
~ tc(proj1Just(just(nil)),proj2App(app(X1,var(X2),X3)),X4),
inference(scs_inference,[],[i_0_212,i_0_263,i_0_336,i_0_74,i_0_340,i_0_101,i_0_127,i_0_128]) ).
cnf(i_0_343,plain,
index(cons(X1,cons(X2,nil)),suc(suc(X3))) = proj1Suc(suc(nothing)),
inference(scs_inference,[],[i_0_212,i_0_263,i_0_331,i_0_336,i_0_270,i_0_74,i_0_340,i_0_101,i_0_127,i_0_128,i_0_102]) ).
cnf(i_0_375,plain,
head(cons(nothing,X1)) = index(cons(X2,nil),suc(X3)),
inference(rename_variables,[],[i_0_336]) ).
cnf(i_0_916,plain,
~ tc(proj2App(app(X1,proj3App(app(X2,X3,nil)),X4)),proj1Arr(arr(var(X5),X6)),X7),
inference(scs_inference,[],[i_0_74,i_0_910,i_0_915,i_0_737,i_0_907,i_0_332,i_0_150,i_0_289,i_0_280,i_0_130,i_0_69,i_0_66,i_0_129,i_0_65,i_0_128,i_0_127]) ).
cnf(i_0_345,plain,
proj1Suc(suc(nothing)) = index(cons(X1,cons(X2,nil)),suc(suc(X3))),
inference(scs_inference,[],[i_0_343,i_0_101]) ).
cnf(i_0_346,plain,
~ tc(proj1App(app(nil,X1,X2)),head(cons(var(X3),X4)),X5),
inference(scs_inference,[],[i_0_224,i_0_343,i_0_75,i_0_101,i_0_127]) ).
cnf(i_0_348,plain,
~ tc(proj1Just(just(nil)),proj1App(app(var(X1),X2,X3)),X4),
inference(scs_inference,[],[i_0_224,i_0_263,i_0_343,i_0_75,i_0_347,i_0_101,i_0_127,i_0_128]) ).
cnf(i_0_350,plain,
index(cons(X1,cons(X2,nil)),suc(suc(X3))) = proj1Lam(lam(nothing)),
inference(scs_inference,[],[i_0_224,i_0_263,i_0_343,i_0_294,i_0_75,i_0_347,i_0_101,i_0_127,i_0_128,i_0_102]) ).
cnf(i_0_402,plain,
~ tc(proj2App(app(X1,nil,X2)),var(X3),X4),
inference(scs_inference,[],[i_0_339,i_0_389,i_0_84,i_0_80,i_0_101,i_0_76,i_0_128]) ).
cnf(i_0_403,plain,
~ tc(proj2App(app(X1,nil,X2)),tail(cons(X3,var(X4))),X5),
inference(rename_variables,[],[i_0_339]) ).
cnf(i_0_405,plain,
~ tc(head(cons(nil,X1)),proj1Var(var(var(X2))),X3),
inference(scs_inference,[],[i_0_339,i_0_140,i_0_389,i_0_84,i_0_80,i_0_101,i_0_76,i_0_128,i_0_127]) ).
cnf(i_0_1840,plain,
index(cons(X1,nil),suc(X2)) = head(cons(nothing,X3)),
inference(rename_variables,[],[i_0_338]) ).
cnf(i_0_351,plain,
proj1Lam(lam(nothing)) = index(cons(X1,cons(X2,nil)),suc(suc(X3))),
inference(scs_inference,[],[i_0_350,i_0_101]) ).
cnf(i_0_352,plain,
~ tc(proj1Lam(lam(nil)),proj3App(app(X1,X2,var(X3))),X4),
inference(scs_inference,[],[i_0_235,i_0_350,i_0_92,i_0_101,i_0_127]) ).
cnf(i_0_354,plain,
~ tc(proj1Suc(suc(nil)),var(X1),X2),
inference(scs_inference,[],[i_0_271,i_0_235,i_0_350,i_0_152,i_0_92,i_0_101,i_0_127,i_0_128]) ).
cnf(i_0_356,plain,
proj1Suc(suc(nothing)) = index(cons(X1,nil),suc(X2)),
inference(scs_inference,[],[i_0_271,i_0_235,i_0_350,i_0_345,i_0_309,i_0_152,i_0_92,i_0_101,i_0_127,i_0_128,i_0_102]) ).
cnf(i_0_358,plain,
~ tc(proj1Suc(suc(nil)),app(var(X1),X2,X3),X4),
inference(scs_inference,[],[i_0_271,i_0_235,i_0_350,i_0_345,i_0_309,i_0_152,i_0_92,i_0_101,i_0_127,i_0_128,i_0_102,i_0_66]) ).
cnf(i_0_434,plain,
~ tc(proj1App(app(nil,X1,X2)),head(cons(var(X3),X4)),X5),
inference(rename_variables,[],[i_0_346]) ).
cnf(i_0_649,plain,
~ tc(proj2App(app(X1,nil,X2)),proj2App(app(X3,var(X4),X5)),X6),
inference(scs_inference,[],[i_0_402,i_0_74,i_0_128]) ).
cnf(i_0_651,plain,
~ tc(proj2App(app(X1,nil,X2)),proj2Arr(arr(X3,var(X4))),X5),
inference(scs_inference,[],[i_0_402,i_0_194,i_0_74,i_0_650,i_0_128,i_0_127]) ).
cnf(i_0_685,plain,
~ tc(proj2App(app(X1,nil,X2)),head(cons(var(X3),X4)),X5),
inference(scs_inference,[],[i_0_402,i_0_212,i_0_84,i_0_684,i_0_127,i_0_128]) ).
cnf(i_0_749,plain,
~ tc(proj2App(app(X1,nil,X2)),proj1Just(just(var(X3))),X4),
inference(scs_inference,[],[i_0_402,i_0_93,i_0_128]) ).
cnf(i_0_2457,plain,
~ tc(proj2App(app(X1,nil,X2)),var(X3),X4),
inference(rename_variables,[],[i_0_402]) ).
cnf(i_0_360,plain,
~ tc(proj1Suc(suc(nil)),app(app(var(X1),X2,X3),X4,X5),X6),
inference(scs_inference,[],[i_0_358,i_0_66]) ).
cnf(i_0_361,plain,
~ tc(proj1Suc(suc(nil)),app(var(X1),X2,X3),X4),
inference(rename_variables,[],[i_0_358]) ).
cnf(i_0_363,plain,
index(cons(X1,nil),suc(X2)) = proj1Suc(suc(nothing)),
inference(scs_inference,[],[i_0_358,i_0_356,i_0_66,i_0_101]) ).
cnf(i_0_364,plain,
~ tc(proj1Suc(suc(nil)),proj1Just(just(var(X1))),X2),
inference(scs_inference,[],[i_0_354,i_0_358,i_0_356,i_0_93,i_0_66,i_0_101,i_0_128]) ).
cnf(i_0_366,plain,
~ tc(proj1Just(just(nil)),proj1Lam(lam(var(X1))),X2),
inference(scs_inference,[],[i_0_354,i_0_358,i_0_160,i_0_356,i_0_93,i_0_365,i_0_66,i_0_101,i_0_128,i_0_127]) ).
cnf(i_0_368,plain,
proj1Lam(lam(nothing)) = index(cons(X1,nil),suc(X2)),
inference(scs_inference,[],[i_0_354,i_0_358,i_0_160,i_0_356,i_0_287,i_0_93,i_0_365,i_0_66,i_0_101,i_0_128,i_0_127,i_0_102]) ).
cnf(i_0_390,plain,
~ tc(proj1Suc(suc(nil)),tail(cons(X1,var(X2))),X3),
inference(scs_inference,[],[i_0_354,i_0_83,i_0_101,i_0_128]) ).
cnf(i_0_392,plain,
~ tc(tail(cons(X1,nil)),app(var(X2),X3,X4),X5),
inference(scs_inference,[],[i_0_306,i_0_354,i_0_83,i_0_391,i_0_101,i_0_128,i_0_127]) ).
cnf(i_0_475,plain,
~ tc(proj1Lam(lam(nil)),proj3App(app(X1,X2,var(X3))),X4),
inference(rename_variables,[],[i_0_352]) ).
cnf(i_0_1897,plain,
~ tc(proj2App(app(X1,nil,X2)),app(X3,proj2App(app(X4,var(X5),X6)),X7),X8),
inference(scs_inference,[],[i_0_649,i_0_67]) ).
cnf(i_0_1899,plain,
~ tc(cons(arr(a,arr(b,c)),proj1Just(just(nil))),X1,arr(b,arr(a,c))),
inference(scs_inference,[],[i_0_649,i_0_170,i_0_67,i_0_69]) ).
cnf(i_0_1942,plain,
~ tc(proj2App(app(X1,nil,X2)),app(X3,proj2Arr(arr(X4,var(X5))),X6),X7),
inference(scs_inference,[],[i_0_651,i_0_67]) ).
cnf(i_0_2177,plain,
~ tc(proj2App(app(X1,nil,X2)),app(X3,head(cons(var(X4),X5)),X6),X7),
inference(scs_inference,[],[i_0_685,i_0_67]) ).
cnf(i_0_2594,plain,
~ tc(proj2App(app(X1,nil,X2)),app(X3,proj1Just(just(var(X4))),X5),X6),
inference(scs_inference,[],[i_0_749,i_0_67]) ).
cnf(i_0_369,plain,
index(cons(X1,nil),suc(X2)) = proj1Lam(lam(nothing)),
inference(scs_inference,[],[i_0_368,i_0_101]) ).
cnf(i_0_370,plain,
~ tc(proj1Suc(suc(nil)),proj1Suc(suc(var(X1))),X2),
inference(scs_inference,[],[i_0_354,i_0_368,i_0_94,i_0_101,i_0_128]) ).
cnf(i_0_372,plain,
~ tc(proj1Suc(suc(nil)),proj2App(app(X1,var(X2),X3)),X4),
inference(scs_inference,[],[i_0_244,i_0_354,i_0_368,i_0_94,i_0_371,i_0_101,i_0_128,i_0_127]) ).
cnf(i_0_374,plain,
proj1Lam(lam(index(nil,X1))) = index(cons(X2,nil),suc(X3)),
inference(scs_inference,[],[i_0_244,i_0_354,i_0_230,i_0_368,i_0_336,i_0_94,i_0_371,i_0_101,i_0_128,i_0_127,i_0_102]) ).
cnf(i_0_985,plain,
~ tc(tail(cons(X1,nil)),app(X2,app(var(X3),X4,X5),X6),X7),
inference(scs_inference,[],[i_0_392,i_0_67]) ).
cnf(i_0_987,plain,
~ tc(cons(X1,nil),lam(var(suc(suc(X2)))),arr(X3,X4)),
inference(scs_inference,[],[i_0_392,i_0_326,i_0_67,i_0_68]) ).
cnf(i_0_989,plain,
arr(proj3App(app(X1,X2,nothing)),X3) = arr(index(nil,X4),X3),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103]) ).
cnf(i_0_990,plain,
arr(X1,proj3App(app(X2,X3,nothing))) = arr(X1,index(nil,X4)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104]) ).
cnf(i_0_991,plain,
proj3App(proj3App(app(X1,X2,nothing))) = proj3App(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105]) ).
cnf(i_0_992,plain,
proj2App(proj3App(app(X1,X2,nothing))) = proj2App(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106]) ).
cnf(i_0_993,plain,
proj1App(proj3App(app(X1,X2,nothing))) = proj1App(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107]) ).
cnf(i_0_994,plain,
suc(proj3App(app(X1,X2,nothing))) = suc(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108]) ).
cnf(i_0_995,plain,
tail(proj3App(app(X1,X2,nothing))) = tail(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109]) ).
cnf(i_0_996,plain,
head(proj3App(app(X1,X2,nothing))) = head(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110]) ).
cnf(i_0_997,plain,
proj1Var(proj3App(app(X1,X2,nothing))) = proj1Var(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111]) ).
cnf(i_0_998,plain,
proj1Lam(proj3App(app(X1,X2,nothing))) = proj1Lam(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112]) ).
cnf(i_0_999,plain,
proj1Just(proj3App(app(X1,X2,nothing))) = proj1Just(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113]) ).
cnf(i_0_1000,plain,
proj1Suc(proj3App(app(X1,X2,nothing))) = proj1Suc(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114]) ).
cnf(i_0_1001,plain,
app(proj3App(app(X1,X2,nothing)),X3,X4) = app(index(nil,X5),X3,X4),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114,i_0_115]) ).
cnf(i_0_1002,plain,
app(X1,proj3App(app(X2,X3,nothing)),X4) = app(X1,index(nil,X5),X4),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114,i_0_115,i_0_116]) ).
cnf(i_0_1003,plain,
app(X1,X2,proj3App(app(X3,X4,nothing))) = app(X1,X2,index(nil,X5)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114,i_0_115,i_0_116,i_0_117]) ).
cnf(i_0_1004,plain,
cons(proj3App(app(X1,X2,nothing)),X3) = cons(index(nil,X4),X3),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114,i_0_115,i_0_116,i_0_117,i_0_118]) ).
cnf(i_0_1005,plain,
cons(X1,proj3App(app(X2,X3,nothing))) = cons(X1,index(nil,X4)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114,i_0_115,i_0_116,i_0_117,i_0_118,i_0_119]) ).
cnf(i_0_1006,plain,
lam(proj3App(app(X1,X2,nothing))) = lam(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114,i_0_115,i_0_116,i_0_117,i_0_118,i_0_119,i_0_120]) ).
cnf(i_0_1007,plain,
var(proj3App(app(X1,X2,nothing))) = var(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114,i_0_115,i_0_116,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121]) ).
cnf(i_0_1008,plain,
index(proj3App(app(X1,X2,nothing)),X3) = index(index(nil,X4),X3),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114,i_0_115,i_0_116,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122]) ).
cnf(i_0_1009,plain,
index(X1,proj3App(app(X2,X3,nothing))) = index(X1,index(nil,X4)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114,i_0_115,i_0_116,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123]) ).
cnf(i_0_1010,plain,
just(proj3App(app(X1,X2,nothing))) = just(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114,i_0_115,i_0_116,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124]) ).
cnf(i_0_1011,plain,
proj1Arr(proj3App(app(X1,X2,nothing))) = proj1Arr(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114,i_0_115,i_0_116,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125]) ).
cnf(i_0_1012,plain,
proj2Arr(proj3App(app(X1,X2,nothing))) = proj2Arr(index(nil,X3)),
inference(scs_inference,[],[i_0_789,i_0_392,i_0_326,i_0_67,i_0_68,i_0_103,i_0_104,i_0_105,i_0_106,i_0_107,i_0_108,i_0_109,i_0_110,i_0_111,i_0_112,i_0_113,i_0_114,i_0_115,i_0_116,i_0_117,i_0_118,i_0_119,i_0_120,i_0_121,i_0_122,i_0_123,i_0_124,i_0_125,i_0_126]) ).
cnf(i_0_1944,plain,
~ tc(cons(b,cons(arr(a,arr(b,c)),proj1Just(just(nil)))),X1,arr(a,c)),
inference(scs_inference,[],[i_0_651,i_0_1899,i_0_67,i_0_69]) ).
cnf(i_0_1945,plain,
~ tc(cons(arr(a,arr(b,c)),proj1Just(just(nil))),X1,arr(b,arr(a,c))),
inference(rename_variables,[],[i_0_1899]) ).
cnf(i_0_376,plain,
index(cons(X1,nil),suc(X2)) = proj1Lam(lam(index(nil,X3))),
inference(scs_inference,[],[i_0_374,i_0_101]) ).
cnf(i_0_377,plain,
~ tc(proj1Suc(suc(nil)),proj2Arr(arr(X1,var(X2))),X3),
inference(scs_inference,[],[i_0_354,i_0_374,i_0_81,i_0_101,i_0_128]) ).
cnf(i_0_379,plain,
~ tc(proj2Arr(arr(X1,nil)),proj1App(app(var(X2),X3,X4)),X5),
inference(scs_inference,[],[i_0_251,i_0_354,i_0_374,i_0_81,i_0_378,i_0_101,i_0_128,i_0_127]) ).
cnf(i_0_381,plain,
index(cons(X1,nil),suc(X2)) = proj2Arr(arr(X3,nothing)),
inference(scs_inference,[],[i_0_251,i_0_354,i_0_374,i_0_369,i_0_210,i_0_81,i_0_378,i_0_101,i_0_128,i_0_127,i_0_102]) ).
cnf(i_0_1801,plain,
index(X1,proj3App(app(X2,X3,nothing))) = index(X1,index(nil,X4)),
inference(rename_variables,[],[i_0_1009]) ).
cnf(i_0_1985,plain,
index(proj3App(app(X1,X2,nothing)),X3) = index(index(nil,X4),X3),
inference(rename_variables,[],[i_0_1008]) ).
cnf(i_0_2023,plain,
arr(X1,proj3App(app(X2,X3,nothing))) = arr(X1,index(nil,X4)),
inference(rename_variables,[],[i_0_990]) ).
cnf(i_0_2033,plain,
~ tc(cons(b,cons(arr(a,arr(b,c)),proj1Just(just(nil)))),X1,arr(a,c)),
inference(rename_variables,[],[i_0_1944]) ).
cnf(i_0_2126,plain,
app(X1,X2,proj3App(app(X3,X4,nothing))) = app(X1,X2,index(nil,X5)),
inference(rename_variables,[],[i_0_1003]) ).
cnf(i_0_382,plain,
proj2Arr(arr(X1,nothing)) = index(cons(X2,nil),suc(X3)),
inference(scs_inference,[],[i_0_381,i_0_101]) ).
cnf(i_0_383,plain,
~ tc(proj1Suc(suc(nil)),proj1Arr(arr(var(X1),X2)),X3),
inference(scs_inference,[],[i_0_354,i_0_381,i_0_82,i_0_101,i_0_128]) ).
cnf(i_0_385,plain,
~ tc(proj1Arr(arr(nil,X1)),app(app(var(X2),X3,X4),X5,X6),X7),
inference(scs_inference,[],[i_0_316,i_0_354,i_0_381,i_0_82,i_0_384,i_0_101,i_0_128,i_0_127]) ).
cnf(i_0_387,plain,
nothing != index(cons(X1,X2),zero),
inference(scs_inference,[],[i_0_316,i_0_354,i_0_381,i_0_95,i_0_82,i_0_384,i_0_80,i_0_101,i_0_128,i_0_127,i_0_102]) ).
cnf(i_0_395,plain,
index(cons(X1,nil),suc(X2)) = proj2Arr(arr(X3,nothing)),
inference(rename_variables,[],[i_0_381]) ).
cnf(i_0_612,plain,
index(cons(X1,nil),suc(X2)) = proj2Arr(arr(X3,nothing)),
inference(rename_variables,[],[i_0_381]) ).
cnf(i_0_394,plain,
proj2Arr(arr(X1,nothing)) = proj2Arr(arr(X2,nothing)),
inference(scs_inference,[],[i_0_306,i_0_354,i_0_382,i_0_381,i_0_83,i_0_391,i_0_101,i_0_128,i_0_127,i_0_102]) ).
cnf(i_0_396,plain,
~ tc(tail(cons(X1,nil)),app(app(var(X2),X3,X4),X5,X6),X7),
inference(scs_inference,[],[i_0_306,i_0_354,i_0_382,i_0_381,i_0_83,i_0_391,i_0_101,i_0_128,i_0_127,i_0_102,i_0_66]) ).
cnf(i_0_407,plain,
nothing != index(cons(X1,cons(X2,X3)),suc(zero)),
inference(scs_inference,[],[i_0_339,i_0_140,i_0_389,i_0_387,i_0_79,i_0_84,i_0_80,i_0_101,i_0_76,i_0_128,i_0_127,i_0_102]) ).
cnf(c_0_1954,plain,
( tc(X1,var(X2),X3)
| X4 != X3
| index(X1,X2) != just(X4) ),
i_0_76 ).
cnf(c_0_1955,plain,
~ tc(cons(b,cons(arr(a,arr(b,c)),proj1Just(just(nil)))),X1,arr(a,c)),
i_0_1944 ).
cnf(c_0_1956,plain,
proj1Just(just(X1)) = X1,
i_0_93 ).
cnf(c_0_1957,plain,
( tc(X1,var(X2),X3)
| index(X1,X2) != just(X3) ),
inference(er,[status(thm)],[c_0_1954]) ).
cnf(c_0_1958,plain,
index(cons(X1,X2),zero) = just(X1),
i_0_80 ).
cnf(c_0_1959,plain,
~ tc(cons(b,cons(arr(a,arr(b,c)),nil)),X1,arr(a,c)),
inference(rw,[status(thm)],[c_0_1955,c_0_1956]) ).
cnf(c_0_1960,plain,
( tc(X1,lam(X2),arr(X3,X4))
| ~ tc(cons(X3,X1),X2,X4) ),
i_0_69 ).
cnf(c_0_1961,plain,
( tc(X1,var(X2),X3)
| index(X1,X2) != index(cons(X3,X4),zero) ),
inference(spm,[status(thm)],[c_0_1957,c_0_1958]) ).
cnf(c_0_1962,plain,
index(X1,X2) = index(cons(X3,X1),suc(X2)),
i_0_279 ).
cnf(c_0_1963,plain,
~ tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X1,c),
inference(spm,[status(thm)],[c_0_1959,c_0_1960]) ).
cnf(c_0_1964,plain,
( tc(X1,app(X2,X3,X4),X5)
| ~ tc(X1,X2,arr(X4,X5))
| ~ tc(X1,X3,X4) ),
i_0_65 ).
cnf(c_0_1965,plain,
( tc(cons(X1,X2),var(suc(X3)),X4)
| index(X2,X3) != index(cons(X4,X5),zero) ),
inference(spm,[status(thm)],[c_0_1961,c_0_1962]) ).
cnf(c_0_1966,plain,
( ~ tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X1,arr(X2,c))
| ~ tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X3,X2) ),
inference(spm,[status(thm)],[c_0_1963,c_0_1964]) ).
cnf(c_0_1967,plain,
( tc(cons(X1,cons(X2,X3)),var(suc(suc(X4))),X5)
| index(X3,X4) != index(cons(X5,X6),zero) ),
inference(spm,[status(thm)],[c_0_1965,c_0_1962]) ).
cnf(c_0_1968,plain,
( ~ tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X1,arr(X2,arr(X3,c)))
| ~ tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X4,X3)
| ~ tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X5,X2) ),
inference(spm,[status(thm)],[c_0_1966,c_0_1964]) ).
cnf(c_0_1969,plain,
tc(cons(X1,cons(X2,cons(X3,X4))),var(suc(suc(zero))),X3),
inference(er,[status(thm)],[c_0_1967]) ).
cnf(c_0_1970,plain,
( ~ tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X1,b)
| ~ tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X2,a) ),
inference(spm,[status(thm)],[c_0_1968,c_0_1969]) ).
cnf(c_0_1971,plain,
tc(cons(X1,cons(X2,X3)),var(suc(zero)),X2),
inference(er,[status(thm)],[c_0_1965]) ).
cnf(c_0_1972,plain,
tc(cons(X1,X2),var(zero),proj1Var(var(X1))),
i_0_959 ).
cnf(c_0_1973,plain,
proj1Var(var(X1)) = X1,
i_0_91 ).
cnf(c_0_1974,plain,
~ tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),X1,a),
inference(spm,[status(thm)],[c_0_1970,c_0_1971]) ).
cnf(c_0_1975,plain,
tc(cons(X1,X2),var(zero),X1),
inference(rw,[status(thm)],[c_0_1972,c_0_1973]) ).
cnf(c_0_1976,plain,
$false,
inference(spm,[status(thm)],[c_0_1974,c_0_1975]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX220+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.32 % Computer : n021.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Tue May 5 07:59:25 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 83.14/41.83 % Version : CSE_E---1.7
% 83.14/41.83 % Problem : theBenchmark.p
% 83.14/41.83 % SZS status Theorem for theBenchmark.p
% 83.14/41.83 % SZS output start CNFRefutation
% See solution above
% 89.15/47.89 % Total time : 41.463s
%------------------------------------------------------------------------------