%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW643_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:40:35 PM UTC 2026
% Result : Theorem 1.18s 0.45s
% Output : Refutation 1.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW643_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.17 % Computer : n004.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Mon Sep 28 14:23:37 UTC 2026
% 0.06/0.17 % CPUTime :
% 0.06/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.20 Running first-order model finding
% 0.06/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.18/0.45 % (383387)Will run a generic schedule for satisfiability detection.
% 1.18/0.45 % (383394)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2548767913:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.18/0.45 % (383393)% WARNING: option uhcvi not known.
% 1.18/0.45 % (383392)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3347429412_2999 on theBenchmark for (2999ds/0Mi)
% 1.18/0.45 % (383393)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=556721328:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.18/0.45 % (383395)dis+10_1_sil=32000:sp=arity:random_seed=3263454829:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.18/0.45 % (383396)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=958739669:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.18/0.45 % (383392)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.18/0.45 % (383392)Terminated due to inappropriate strategy.
% 1.18/0.45 % (383392)------------------------------
% 1.18/0.45 % (383392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.45 % (383392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.45 % (383392)CaDiCaL version: 2.1.3
% 1.18/0.45 % (383392)Termination reason: Inappropriate
% 1.18/0.45 % (383392)Time elapsed: 0.003 s
% 1.18/0.45 % (383392)Peak memory usage: 10 MB
% 1.18/0.45 % (383392)Instructions burned: 5 (million)
% 1.18/0.45 % (383392)------------------------------
% 1.18/0.45 % (383392)------------------------------
% 1.18/0.45 % (383398)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1852098447:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.18/0.45 % (383397)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2275671650:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.18/0.45 % (383404)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3562269271:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.18/0.45 % (383404)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.18/0.45 % (383404)Terminated due to inappropriate strategy.
% 1.18/0.45 % (383404)------------------------------
% 1.18/0.45 % (383404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.45 % (383404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.45 % (383404)CaDiCaL version: 2.1.3
% 1.18/0.45 % (383404)Termination reason: Inappropriate
% 1.18/0.45 % (383404)Time elapsed: 0.003 s
% 1.18/0.45 % (383404)Peak memory usage: 10 MB
% 1.18/0.45 % (383404)Instructions burned: 4 (million)
% 1.18/0.45 % (383404)------------------------------
% 1.18/0.45 % (383404)------------------------------
% 1.18/0.45 % (383408)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2859890448:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.18/0.45 % (383397)Instruction limit reached!
% 1.18/0.45 % (383397)------------------------------
% 1.18/0.45 % (383397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.45 % (383397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.45 % (383397)CaDiCaL version: 2.1.3
% 1.18/0.45 % (383397)Termination reason: Instruction limit
% 1.18/0.45 % (383397)Termination phase: Saturation
% 1.18/0.45 % (383397)Time elapsed: 0.049 s
% 1.18/0.45 % (383397)Peak memory usage: 13 MB
% 1.18/0.45 % (383397)Instructions burned: 132 (million)
% 1.18/0.45 % (383395)Instruction limit reached!
% 1.18/0.45 % (383395)------------------------------
% 1.18/0.45 % (383395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.45 % (383395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.45 % (383395)CaDiCaL version: 2.1.3
% 1.18/0.45 % (383395)Termination reason: Instruction limit
% 1.18/0.45 % (383395)Termination phase: Saturation
% 1.18/0.45 % (383395)Time elapsed: 0.069 s
% 1.18/0.45 % (383395)Peak memory usage: 13 MB
% 1.18/0.45 % (383395)Instructions burned: 104 (million)
% 1.18/0.45 % (383410)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=464256363:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.18/0.45 % (383396)Instruction limit reached!
% 1.18/0.45 % (383396)------------------------------
% 1.18/0.45 % (383396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.45 % (383396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.45 % (383396)CaDiCaL version: 2.1.3
% 1.18/0.45 % (383396)Termination reason: Instruction limit
% 1.18/0.45 % (383396)Termination phase: Saturation
% 1.18/0.45 % (383396)Time elapsed: 0.077 s
% 1.18/0.45 % (383396)Peak memory usage: 13 MB
% 1.18/0.45 % (383396)Instructions burned: 116 (million)
% 1.18/0.45 % (383411)ott-21_1_sil=16000:fs=off:random_seed=844402125:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.18/0.45 % (383413)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3968358830:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.18/0.45 % (383398)Instruction limit reached!
% 1.18/0.45 % (383398)------------------------------
% 1.18/0.45 % (383398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.45 % (383398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.45 % (383398)CaDiCaL version: 2.1.3
% 1.18/0.45 % (383398)Termination reason: Instruction limit
% 1.18/0.45 % (383398)Termination phase: Saturation
% 1.18/0.45 % (383398)Time elapsed: 0.100 s
% 1.18/0.45 % (383398)Peak memory usage: 13 MB
% 1.18/0.45 % (383398)Instructions burned: 159 (million)
% 1.18/0.45 % (383416)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1035977515:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.18/0.45 % (383416)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.18/0.45 % (383416)Terminated due to inappropriate strategy.
% 1.18/0.45 % (383416)------------------------------
% 1.18/0.45 % (383416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.45 % (383416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.45 % (383416)CaDiCaL version: 2.1.3
% 1.18/0.45 % (383416)Termination reason: Inappropriate
% 1.18/0.45 % (383416)Time elapsed: 0.002 s
% 1.18/0.45 % (383416)Peak memory usage: 10 MB
% 1.18/0.45 % (383416)Instructions burned: 3 (million)
% 1.18/0.45 % (383416)------------------------------
% 1.18/0.45 % (383416)------------------------------
% 1.18/0.45 % (383408)Instruction limit reached!
% 1.18/0.45 % (383408)------------------------------
% 1.18/0.45 % (383408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.45 % (383408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.45 % (383408)CaDiCaL version: 2.1.3
% 1.18/0.45 % (383408)Termination reason: Instruction limit
% 1.18/0.45 % (383408)Termination phase: Saturation
% 1.18/0.45 % (383408)Time elapsed: 0.088 s
% 1.18/0.45 % (383408)Peak memory usage: 13 MB
% 1.18/0.45 % (383408)Instructions burned: 132 (million)
% 1.18/0.45 % (383418)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3376754245:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.18/0.45 % (383419)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4286133290:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.18/0.45 % (383419)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.18/0.45 % (383419)Terminated due to inappropriate strategy.
% 1.18/0.45 % (383419)------------------------------
% 1.18/0.45 % (383419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.45 % (383419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.45 % (383419)CaDiCaL version: 2.1.3
% 1.18/0.45 % (383419)Termination reason: Inappropriate
% 1.18/0.45 % (383419)Time elapsed: 0.003 s
% 1.18/0.45 % (383419)Peak memory usage: 10 MB
% 1.18/0.45 % (383419)Instructions burned: 4 (million)
% 1.18/0.45 % (383419)------------------------------
% 1.18/0.45 % (383419)------------------------------
% 1.18/0.45 % (383411)Instruction limit reached!
% 1.18/0.45 % (383411)------------------------------
% 1.18/0.45 % (383411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.45 % (383411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.45 % (383411)CaDiCaL version: 2.1.3
% 1.18/0.45 % (383411)Termination reason: Instruction limit
% 1.18/0.45 % (383411)Termination phase: Saturation
% 1.18/0.45 % (383411)Time elapsed: 0.094 s
% 1.18/0.45 % (383411)Peak memory usage: 12 MB
% 1.18/0.45 % (383411)Instructions burned: 182 (million)
% 1.18/0.45 % (383422)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=826304094:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 1.18/0.45 % (383393) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-383387-383393"...
% 1.18/0.45 % (383393)...printing done.
% 1.18/0.45 % (383393)Refutation found. Thanks to Tanya!
% 1.18/0.45 % SZS status Theorem for theBenchmark
% 1.18/0.45 % SZS output start Proof for theBenchmark
% 1.18/0.45 tff(type_def_5, type, uni: $tType).
% 1.18/0.45 tff(type_def_6, type, ty: $tType).
% 1.18/0.45 tff(type_def_7, type, bool1: $tType).
% 1.18/0.45 tff(type_def_8, type, tuple02: $tType).
% 1.18/0.45 tff(type_def_9, type, list_int: $tType).
% 1.18/0.45 tff(func_def_0, type, witness1: ty > uni).
% 1.18/0.45 tff(func_def_1, type, int: ty).
% 1.18/0.45 tff(func_def_2, type, real: ty).
% 1.18/0.45 tff(func_def_3, type, bool: ty).
% 1.18/0.45 tff(func_def_4, type, true1: bool1).
% 1.18/0.45 tff(func_def_5, type, false1: bool1).
% 1.18/0.45 tff(func_def_6, type, match_bool1: (ty * bool1 * uni * uni) > uni).
% 1.18/0.45 tff(func_def_7, type, tuple0: ty).
% 1.18/0.45 tff(func_def_8, type, tuple03: tuple02).
% 1.18/0.45 tff(func_def_9, type, qtmark: ty).
% 1.18/0.45 tff(func_def_12, type, list: ty > ty).
% 1.18/0.45 tff(func_def_13, type, nil: ty > uni).
% 1.18/0.45 tff(func_def_14, type, cons: (ty * uni * uni) > uni).
% 1.18/0.45 tff(func_def_15, type, match_list1: (ty * ty * uni * uni * uni) > uni).
% 1.18/0.45 tff(func_def_16, type, cons_proj_11: (ty * uni) > uni).
% 1.18/0.45 tff(func_def_17, type, cons_proj_21: (ty * uni) > uni).
% 1.18/0.45 tff(func_def_18, type, t2tb: list_int > uni).
% 1.18/0.45 tff(func_def_19, type, tb2t: uni > list_int).
% 1.18/0.45 tff(func_def_20, type, t2tb1: $int > uni).
% 1.18/0.45 tff(func_def_21, type, tb2t1: uni > $int).
% 1.18/0.45 tff(func_def_22, type, infix_plpl: (ty * uni * uni) > uni).
% 1.18/0.45 tff(func_def_23, type, length1: (ty * uni) > $int).
% 1.18/0.45 tff(func_def_27, type, sK0: list_int > $int).
% 1.18/0.45 tff(func_def_28, type, sK1: list_int > $int).
% 1.18/0.45 tff(func_def_29, type, sK2: list_int > list_int).
% 1.18/0.45 tff(func_def_30, type, sK3: list_int > $int).
% 1.18/0.45 tff(func_def_31, type, sK4: ($int * list_int) > $int).
% 1.18/0.45 tff(func_def_32, type, sK5: (ty * uni * uni) > uni).
% 1.18/0.45 tff(func_def_33, type, sK6: (ty * uni * uni) > uni).
% 1.18/0.45 tff(func_def_34, type, sK7: (list_int * list_int) > $int).
% 1.18/0.45 tff(func_def_35, type, sK8: (list_int * list_int) > $int).
% 1.18/0.45 tff(func_def_36, type, sK9: $int).
% 1.18/0.45 tff(func_def_37, type, sK10: list_int).
% 1.18/0.45 tff(func_def_38, type, sK11: $int).
% 1.18/0.45 tff(func_def_39, type, sK12: list_int).
% 1.18/0.45 tff(func_def_40, type, sK13: bool1).
% 1.18/0.45 tff(func_def_41, type, sK14: $int).
% 1.18/0.45 tff(func_def_42, type, sK15: list_int).
% 1.18/0.45 tff(pred_def_1, type, sort1: (ty * uni) > $o).
% 1.18/0.45 tff(pred_def_3, type, mem: (ty * uni * uni) > $o).
% 1.18/0.45 tff(pred_def_4, type, sorted1: list_int > $o).
% 1.18/0.45 tff(pred_def_6, type, sP16: (list_int * $int * list_int * list_int) > $o).
% 1.18/0.45 tff(f14,axiom,(
% 1.18/0.45 ! [X0 : ty,X1 : uni,X2 : uni] : nil(X0) != cons(X0,X1,X2)),
% 1.18/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',nil_Cons1)).
% 1.18/0.45 tff(f18,axiom,(
% 1.18/0.45 ! [X0 : ty,X1 : uni,X2 : uni] : cons_proj_21(X0,cons(X0,X1,X2)) = X2),
% 1.18/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cons_proj_2_def1)).
% 1.18/0.45 tff(f20,axiom,(
% 1.18/0.45 ! [X0 : ty,X1 : uni] : (sort1(X0,X1) => (~mem(X0,X1,nil(X0)) & ! [X2 : uni,X3 : uni] : (sort1(X0,X2) => (mem(X0,X1,cons(X0,X2,X3)) <=> (X1 = X2 | mem(X0,X1,X3))))))),
% 1.18/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_def)).
% 1.18/0.45 tff(f22,axiom,(
% 1.18/0.45 ! [X0 : list_int] : tb2t(t2tb(X0)) = X0),
% 1.18/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL)).
% 1.18/0.45 tff(f23,axiom,(
% 1.18/0.45 ! [X0 : uni] : t2tb(tb2t(X0)) = X0),
% 1.18/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR)).
% 1.18/0.45 tff(f25,axiom,(
% 1.18/0.45 ! [X0 : $int] : sort1(int,t2tb1(X0))),
% 1.18/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort1)).
% 1.18/0.45 tff(f26,axiom,(
% 1.18/0.45 ! [X0 : $int] : tb2t1(t2tb1(X0)) = X0),
% 1.18/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL1)).
% 1.18/0.45 tff(f27,axiom,(
% 1.18/0.45 ! [X0 : uni] : t2tb1(tb2t1(X0)) = X0),
% 1.18/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR1)).
% 1.18/0.45 tff(f31,axiom,(
% 1.18/0.45 ! [X0 : $int,X1 : list_int] : ((! [X2 : $int] : (mem(int,t2tb1(X2),t2tb(X1)) => $lesseq(X0,X2)) & sorted1(X1)) <=> sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1)))))),
% 1.18/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',sorted_mem)).
% 1.18/0.45 tff(f43,axiom,(
% 1.18/0.45 ! [X0 : $int,X1 : $int,X2 : list_int] : ($less(X0,X1) => (sorted1(tb2t(cons(int,t2tb1(X1),t2tb(X2)))) => ~mem(int,t2tb1(X0),cons(int,t2tb1(X1),t2tb(X2)))))),
% 1.18/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',sorted_not_mem)).
% 1.18/0.45 tff(f44,conjecture,(
% 1.18/0.45 ! [X0 : $int,X1 : list_int] : (sorted1(X1) => ((X1 = tb2t(nil(int)) => ~mem(int,t2tb1(X0),t2tb(X1))) & ! [X2 : $int,X3 : list_int] : (X1 = tb2t(cons(int,t2tb1(X2),t2tb(X3))) => ((X0 = X2 => mem(int,t2tb1(X0),t2tb(X1))) & (X0 != X2 => (($less(X2,X0) => (X1 != tb2t(nil(int)) & ! [X4 : $int,X5 : list_int] : (X1 = tb2t(cons(int,t2tb1(X4),t2tb(X5))) => X5 = X3) & sorted1(X3) & ! [X6 : bool1] : ((X6 = true1 <=> mem(int,t2tb1(X0),t2tb(X3))) => (X6 = true1 <=> mem(int,t2tb1(X0),t2tb(X1)))))) & (~$less(X2,X0) => ~mem(int,t2tb1(X0),t2tb(X1)))))))))),
% 1.18/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_find)).
% 1.18/0.45 tff(f45,negated_conjecture,(
% 1.18/0.45 ~ ! [X0 : $int,X1 : list_int] : (sorted1(X1) => ((X1 = tb2t(nil(int)) => ~mem(int,t2tb1(X0),t2tb(X1))) & ! [X2 : $int,X3 : list_int] : (X1 = tb2t(cons(int,t2tb1(X2),t2tb(X3))) => ((X0 = X2 => mem(int,t2tb1(X0),t2tb(X1))) & (X0 != X2 => (($less(X2,X0) => (X1 != tb2t(nil(int)) & ! [X4 : $int,X5 : list_int] : (X1 = tb2t(cons(int,t2tb1(X4),t2tb(X5))) => X5 = X3) & sorted1(X3) & ! [X6 : bool1] : ((X6 = true1 <=> mem(int,t2tb1(X0),t2tb(X3))) => (X6 = true1 <=> mem(int,t2tb1(X0),t2tb(X1)))))) & (~$less(X2,X0) => ~mem(int,t2tb1(X0),t2tb(X1)))))))))),
% 1.18/0.45 inference(negated_conjecture,[status(cth)],[f44])).
% 1.18/0.45 tff(f49,plain,(
% 1.18/0.45 ! [X0 : $int,X1 : list_int] : ((! [X2 : $int] : (mem(int,t2tb1(X2),t2tb(X1)) => ~$less(X2,X0)) & sorted1(X1)) <=> sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1)))))),
% 1.18/0.45 inference(theory_normalization,[],[f31])).
% 1.18/0.45 tff(f59,definition,(
% 1.18/0.45 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | $less(X1,X0) | X0 = X1) )),
% 1.18/0.45 introduced(theory,[tha_order_totality])).
% 1.18/0.45 tff(f78,plain,(
% 1.18/0.45 ! [X0 : ty,X1 : uni] : ((~mem(X0,X1,nil(X0)) & ! [X2 : uni,X3 : uni] : ((mem(X0,X1,cons(X0,X2,X3)) <=> (X1 = X2 | mem(X0,X1,X3))) | ~sort1(X0,X2))) | ~sort1(X0,X1))),
% 1.18/0.45 inference(ennf_transformation,[],[f20])).
% 1.18/0.45 tff(f83,plain,(
% 1.18/0.45 ! [X0 : $int,X1 : list_int] : ((! [X2 : $int] : (~$less(X2,X0) | ~mem(int,t2tb1(X2),t2tb(X1))) & sorted1(X1)) <=> sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1)))))),
% 1.18/0.45 inference(ennf_transformation,[],[f49])).
% 1.18/0.45 tff(f87,plain,(
% 1.18/0.45 ! [X0 : $int,X1 : $int,X2 : list_int] : ((~mem(int,t2tb1(X0),cons(int,t2tb1(X1),t2tb(X2))) | ~sorted1(tb2t(cons(int,t2tb1(X1),t2tb(X2))))) | ~$less(X0,X1))),
% 1.18/0.45 inference(ennf_transformation,[],[f43])).
% 1.18/0.45 tff(f88,plain,(
% 1.18/0.45 ! [X0 : $int,X1 : $int,X2 : list_int] : (~mem(int,t2tb1(X0),cons(int,t2tb1(X1),t2tb(X2))) | ~sorted1(tb2t(cons(int,t2tb1(X1),t2tb(X2)))) | ~$less(X0,X1))),
% 1.18/0.45 inference(flattening,[],[f87])).
% 1.18/0.45 tff(f89,plain,(
% 1.18/0.45 ? [X0 : $int,X1 : list_int] : (((mem(int,t2tb1(X0),t2tb(X1)) & X1 = tb2t(nil(int))) | ? [X2 : $int,X3 : list_int] : (((~mem(int,t2tb1(X0),t2tb(X1)) & X0 = X2) | ((((tb2t(nil(int)) = X1 | ? [X4 : $int,X5 : list_int] : (X3 != X5 & X1 = tb2t(cons(int,t2tb1(X4),t2tb(X5)))) | ~sorted1(X3) | ? [X6 : bool1] : ((X6 = true1 <~> mem(int,t2tb1(X0),t2tb(X1))) & (X6 = true1 <=> mem(int,t2tb1(X0),t2tb(X3))))) & $less(X2,X0)) | (mem(int,t2tb1(X0),t2tb(X1)) & ~$less(X2,X0))) & X0 != X2)) & X1 = tb2t(cons(int,t2tb1(X2),t2tb(X3))))) & sorted1(X1))),
% 1.18/0.45 inference(ennf_transformation,[],[f45])).
% 1.18/0.45 tff(f103,plain,(
% 1.18/0.45 ( ! [X2 : uni,X0 : ty,X1 : uni] : (nil(X0) != cons(X0,X1,X2)) )),
% 1.18/0.45 inference(cnf_transformation,[],[f14])).
% 1.18/0.45 tff(f107,plain,(
% 1.18/0.45 ( ! [X2 : uni,X0 : ty,X1 : uni] : (cons_proj_21(X0,cons(X0,X1,X2)) = X2) )),
% 1.18/0.45 inference(cnf_transformation,[],[f18])).
% 1.18/0.45 tff(f109,plain,(
% 1.18/0.45 ( ! [X2 : uni,X3 : uni,X0 : ty,X1 : uni] : (~sort1(X0,X1) | ~sort1(X0,X2) | mem(X0,X1,X3) | X1 = X2 | ~mem(X0,X1,cons(X0,X2,X3))) )),
% 1.18/0.45 inference(cnf_transformation,[],[f78])).
% 1.18/0.45 tff(f110,plain,(
% 1.18/0.45 ( ! [X2 : uni,X3 : uni,X0 : ty,X1 : uni] : (~sort1(X0,X1) | ~sort1(X0,X2) | ~mem(X0,X1,X3) | mem(X0,X1,cons(X0,X2,X3))) )),
% 1.18/0.45 inference(cnf_transformation,[],[f78])).
% 1.18/0.45 tff(f111,plain,(
% 1.18/0.45 ( ! [X2 : uni,X3 : uni,X0 : ty,X1 : uni] : (~sort1(X0,X1) | ~sort1(X0,X2) | X1 != X2 | mem(X0,X1,cons(X0,X2,X3))) )),
% 1.18/0.45 inference(cnf_transformation,[],[f78])).
% 1.18/0.45 tff(f112,plain,(
% 1.18/0.45 ( ! [X0 : ty,X1 : uni] : (~sort1(X0,X1) | ~mem(X0,X1,nil(X0))) )),
% 1.18/0.45 inference(cnf_transformation,[],[f78])).
% 1.18/0.45 tff(f114,plain,(
% 1.18/0.45 ( ! [X0 : list_int] : (tb2t(t2tb(X0)) = X0) )),
% 1.18/0.45 inference(cnf_transformation,[],[f22])).
% 1.18/0.45 tff(f115,plain,(
% 1.18/0.45 ( ! [X0 : uni] : (t2tb(tb2t(X0)) = X0) )),
% 1.18/0.45 inference(cnf_transformation,[],[f23])).
% 1.18/0.45 tff(f117,plain,(
% 1.18/0.45 ( ! [X0 : $int] : (sort1(int,t2tb1(X0))) )),
% 1.18/0.45 inference(cnf_transformation,[],[f25])).
% 1.18/0.45 tff(f118,plain,(
% 1.18/0.45 ( ! [X0 : $int] : (tb2t1(t2tb1(X0)) = X0) )),
% 1.18/0.45 inference(cnf_transformation,[],[f26])).
% 1.18/0.45 tff(f119,plain,(
% 1.18/0.45 ( ! [X0 : uni] : (t2tb1(tb2t1(X0)) = X0) )),
% 1.18/0.45 inference(cnf_transformation,[],[f27])).
% 1.18/0.45 tff(f128,plain,(
% 1.18/0.45 ( ! [X0 : $int,X1 : list_int] : (~sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1)))) | sorted1(X1)) )),
% 1.18/0.45 inference(cnf_transformation,[],[f83])).
% 1.18/0.45 tff(f152,plain,(
% 1.18/0.45 ( ! [X2 : list_int,X0 : $int,X1 : $int] : (~$less(X0,X1) | ~sorted1(tb2t(cons(int,t2tb1(X1),t2tb(X2)))) | ~mem(int,t2tb1(X0),cons(int,t2tb1(X1),t2tb(X2)))) )),
% 1.18/0.45 inference(cnf_transformation,[],[f88])).
% 1.18/0.45 tff(f153,plain,(
% 1.18/0.45 ( ! [X3 : list_int,X1 : list_int,X4 : $int,X5 : list_int] : (~sP16(X5,X4,X3,X1) | tb2t(cons(int,t2tb1(X4),t2tb(X5))) = X1) )),
% 1.18/0.45 inference(cnf_transformation,[],[f89])).
% 1.18/0.45 tff(f154,plain,(
% 1.18/0.45 ( ! [X3 : list_int,X1 : list_int,X4 : $int,X5 : list_int] : (X3 != X5 | ~sP16(X5,X4,X3,X1)) )),
% 1.18/0.45 inference(cnf_transformation,[],[f89])).
% 1.18/0.45 tff(f158,plain,(
% 1.18/0.45 ~$less(sK11,sK9) | true1 != sK13 | ~sorted1(sK12) | sP16(sK15,sK14,sK12,sK10) | ~mem(int,t2tb1(sK9),t2tb(sK10)) | tb2t(nil(int)) = sK10),
% 1.18/0.45 inference(cnf_transformation,[],[f89])).
% 1.18/0.45 tff(f160,plain,(
% 1.18/0.45 true1 = sK13 | ~sorted1(sK12) | sP16(sK15,sK14,sK12,sK10) | tb2t(nil(int)) = sK10 | sK9 = sK11 | mem(int,t2tb1(sK9),t2tb(sK10))),
% 1.18/0.45 inference(cnf_transformation,[],[f89])).
% 1.18/0.45 tff(f161,plain,(
% 1.18/0.45 ~$less(sK11,sK9) | ~mem(int,t2tb1(sK9),t2tb(sK12)) | true1 = sK13 | ~sorted1(sK12) | sP16(sK15,sK14,sK12,sK10) | sK9 = sK11 | tb2t(nil(int)) = sK10),
% 1.18/0.45 inference(cnf_transformation,[],[f89])).
% 1.18/0.45 tff(f170,plain,(
% 1.18/0.45 mem(int,t2tb1(sK9),t2tb(sK12)) | true1 != sK13 | ~sorted1(sK12) | sP16(sK15,sK14,sK12,sK10) | tb2t(nil(int)) = sK10 | sK9 = sK11 | mem(int,t2tb1(sK9),t2tb(sK10))),
% 1.18/0.45 inference(cnf_transformation,[],[f89])).
% 1.18/0.45 tff(f173,plain,(
% 1.18/0.45 sK9 != sK11 | ~mem(int,t2tb1(sK9),t2tb(sK10)) | tb2t(nil(int)) = sK10),
% 1.18/0.45 inference(cnf_transformation,[],[f89])).
% 1.18/0.45 tff(f174,plain,(
% 1.18/0.45 sK10 = tb2t(cons(int,t2tb1(sK11),t2tb(sK12))) | mem(int,t2tb1(sK9),t2tb(sK10))),
% 1.18/0.45 inference(cnf_transformation,[],[f89])).
% 1.18/0.45 tff(f175,plain,(
% 1.18/0.45 sK10 = tb2t(cons(int,t2tb1(sK11),t2tb(sK12))) | tb2t(nil(int)) = sK10),
% 1.18/0.45 inference(cnf_transformation,[],[f89])).
% 1.18/0.45 tff(f176,plain,(
% 1.18/0.45 sorted1(sK10)),
% 1.18/0.45 inference(cnf_transformation,[],[f89])).
% 1.18/0.45 tff(f178,plain,(
% 1.18/0.45 ( ! [X2 : uni,X3 : uni,X0 : ty] : (~sort1(X0,X2) | ~sort1(X0,X2) | mem(X0,X2,cons(X0,X2,X3))) )),
% 1.18/0.45 inference(equality_resolution,[],[f111])).
% 1.18/0.45 tff(f180,plain,(
% 1.18/0.45 ( ! [X1 : list_int,X4 : $int,X5 : list_int] : (~sP16(X5,X4,X5,X1)) )),
% 1.18/0.45 inference(equality_resolution,[],[f154])).
% 1.18/0.45 tff(f181,plain,(
% 1.18/0.45 ( ! [X0 : ty,X1 : uni] : (mem(X0,X1,nil(X0)) | ~sort1(X0,X1)) )),
% 1.18/0.45 inference(consistent_polarity_flipping,[],[f112])).
% 1.18/0.45 tff(f182,plain,(
% 1.18/0.45 ( ! [X2 : uni,X3 : uni,X0 : ty] : (~sort1(X0,X2) | ~sort1(X0,X2) | ~mem(X0,X2,cons(X0,X2,X3))) )),
% 1.18/0.45 inference(consistent_polarity_flipping,[],[f178])).
% 1.18/0.45 tff(f183,plain,(
% 1.18/0.45 ( ! [X2 : uni,X3 : uni,X0 : ty,X1 : uni] : (~mem(X0,X1,cons(X0,X2,X3)) | ~sort1(X0,X2) | mem(X0,X1,X3) | ~sort1(X0,X1)) )),
% 1.18/0.45 inference(consistent_polarity_flipping,[],[f110])).
% 1.18/0.45 tff(f184,plain,(
% 1.18/0.45 ( ! [X2 : uni,X3 : uni,X0 : ty,X1 : uni] : (~mem(X0,X1,X3) | ~sort1(X0,X2) | ~sort1(X0,X1) | X1 = X2 | mem(X0,X1,cons(X0,X2,X3))) )),
% 1.18/0.45 inference(consistent_polarity_flipping,[],[f109])).
% 1.18/0.45 tff(f196,plain,(
% 1.18/0.45 ( ! [X2 : list_int,X0 : $int,X1 : $int] : (~sorted1(tb2t(cons(int,t2tb1(X1),t2tb(X2)))) | ~$less(X0,X1) | mem(int,t2tb1(X0),cons(int,t2tb1(X1),t2tb(X2)))) )),
% 1.18/0.45 inference(consistent_polarity_flipping,[],[f152])).
% 1.18/0.45 tff(f197,plain,(
% 1.18/0.45 sK10 = tb2t(cons(int,t2tb1(sK11),t2tb(sK12))) | ~mem(int,t2tb1(sK9),t2tb(sK10))),
% 1.18/0.45 inference(consistent_polarity_flipping,[],[f174])).
% 1.18/0.45 tff(f198,plain,(
% 1.18/0.45 sK9 != sK11 | mem(int,t2tb1(sK9),t2tb(sK10)) | tb2t(nil(int)) = sK10),
% 1.18/0.45 inference(consistent_polarity_flipping,[],[f173])).
% 1.18/0.45 tff(f201,plain,(
% 1.18/0.45 ~mem(int,t2tb1(sK9),t2tb(sK12)) | true1 != sK13 | ~sorted1(sK12) | sP16(sK15,sK14,sK12,sK10) | tb2t(nil(int)) = sK10 | sK9 = sK11 | ~mem(int,t2tb1(sK9),t2tb(sK10))),
% 1.18/0.45 inference(consistent_polarity_flipping,[],[f170])).
% 1.18/0.45 tff(f210,plain,(
% 1.18/0.45 ~$less(sK11,sK9) | mem(int,t2tb1(sK9),t2tb(sK12)) | true1 = sK13 | ~sorted1(sK12) | sP16(sK15,sK14,sK12,sK10) | sK9 = sK11 | tb2t(nil(int)) = sK10),
% 1.18/0.45 inference(consistent_polarity_flipping,[],[f161])).
% 1.18/0.45 tff(f211,plain,(
% 1.18/0.45 true1 = sK13 | ~sorted1(sK12) | sP16(sK15,sK14,sK12,sK10) | tb2t(nil(int)) = sK10 | sK9 = sK11 | ~mem(int,t2tb1(sK9),t2tb(sK10))),
% 1.18/0.45 inference(consistent_polarity_flipping,[],[f160])).
% 1.18/0.45 tff(f213,plain,(
% 1.18/0.45 ~$less(sK11,sK9) | true1 != sK13 | ~sorted1(sK12) | sP16(sK15,sK14,sK12,sK10) | mem(int,t2tb1(sK9),t2tb(sK10)) | tb2t(nil(int)) = sK10),
% 1.18/0.45 inference(consistent_polarity_flipping,[],[f158])).
% 1.18/0.45 tff(f217,plain,(
% 1.18/0.45 ( ! [X2 : uni,X3 : uni,X0 : ty] : (~mem(X0,X2,cons(X0,X2,X3)) | ~sort1(X0,X2)) )),
% 1.18/0.45 inference(duplicate_literal_removal,[],[f182])).
% 1.18/0.45 tff(f219,definition,(
% 1.18/0.45 spl17_1 <=> tb2t(nil(int)) = sK10),
% 1.18/0.45 introduced(definition,[new_symbols(definition,[spl17_1])],[avatar_definition])).
% 1.18/0.45 tff(f221,plain,(
% 1.18/0.45 tb2t(nil(int)) = sK10 | ~spl17_1),
% 1.18/0.45 inference(avatar_component_clause,[],[f219])).
% 1.18/0.45 tff(f223,definition,(
% 1.18/0.45 spl17_2 <=> sK9 = sK11),
% 1.18/0.45 introduced(definition,[new_symbols(definition,[spl17_2])],[avatar_definition])).
% 1.18/0.45 tff(f224,plain,(
% 1.18/0.45 sK9 != sK11 | spl17_2),
% 1.18/0.45 inference(avatar_component_clause,[],[f223])).
% 1.18/0.45 tff(f225,plain,(
% 1.18/0.45 sK9 = sK11 | ~spl17_2),
% 1.18/0.45 inference(avatar_component_clause,[],[f223])).
% 1.18/0.45 tff(f227,definition,(
% 1.18/0.45 spl17_3 <=> sP16(sK15,sK14,sK12,sK10)),
% 1.18/0.45 introduced(definition,[new_symbols(definition,[spl17_3])],[avatar_definition])).
% 1.18/0.45 tff(f229,plain,(
% 1.18/0.45 sP16(sK15,sK14,sK12,sK10) | ~spl17_3),
% 1.18/0.45 inference(avatar_component_clause,[],[f227])).
% 1.18/0.45 tff(f231,definition,(
% 1.18/0.45 spl17_4 <=> sorted1(sK12)),
% 1.18/0.45 introduced(definition,[new_symbols(definition,[spl17_4])],[avatar_definition])).
% 1.18/0.45 tff(f235,definition,(
% 1.18/0.45 spl17_5 <=> true1 = sK13),
% 1.18/0.45 introduced(definition,[new_symbols(definition,[spl17_5])],[avatar_definition])).
% 1.18/0.45 tff(f239,definition,(
% 1.18/0.45 spl17_6 <=> mem(int,t2tb1(sK9),t2tb(sK10))),
% 1.18/0.45 introduced(definition,[new_symbols(definition,[spl17_6])],[avatar_definition])).
% 1.18/0.45 tff(f240,plain,(
% 1.18/0.45 mem(int,t2tb1(sK9),t2tb(sK10)) | ~spl17_6),
% 1.18/0.45 inference(avatar_component_clause,[],[f239])).
% 1.18/0.45 tff(f241,plain,(
% 1.18/0.45 ~mem(int,t2tb1(sK9),t2tb(sK10)) | spl17_6),
% 1.18/0.45 inference(avatar_component_clause,[],[f239])).
% 1.18/0.45 tff(f243,definition,(
% 1.18/0.45 spl17_7 <=> $less(sK11,sK9)),
% 1.18/0.45 introduced(definition,[new_symbols(definition,[spl17_7])],[avatar_definition])).
% 1.18/0.45 tff(f245,plain,(
% 1.18/0.45 ~$less(sK11,sK9) | spl17_7),
% 1.18/0.45 inference(avatar_component_clause,[],[f243])).
% 1.18/0.45 tff(f249,plain,(
% 1.18/0.45 spl17_1 | spl17_6 | spl17_3 | ~spl17_4 | ~spl17_5 | ~spl17_7),
% 1.18/0.45 inference(avatar_split_clause,[],[f213,f243,f235,f231,f227,f239,f219])).
% 1.18/0.45 tff(f251,plain,(
% 1.18/0.45 ~spl17_6 | spl17_2 | spl17_1 | spl17_3 | ~spl17_4 | spl17_5),
% 1.18/0.45 inference(avatar_split_clause,[],[f211,f235,f231,f227,f219,f223,f239])).
% 1.18/0.45 tff(f253,definition,(
% 1.18/0.45 spl17_8 <=> mem(int,t2tb1(sK9),t2tb(sK12))),
% 1.18/0.45 introduced(definition,[new_symbols(definition,[spl17_8])],[avatar_definition])).
% 1.18/0.45 tff(f255,plain,(
% 1.18/0.45 mem(int,t2tb1(sK9),t2tb(sK12)) | ~spl17_8),
% 1.18/0.45 inference(avatar_component_clause,[],[f253])).
% 1.18/0.45 tff(f256,plain,(
% 1.18/0.45 spl17_1 | spl17_2 | spl17_3 | ~spl17_4 | spl17_5 | spl17_8 | ~spl17_7),
% 1.18/0.45 inference(avatar_split_clause,[],[f210,f243,f253,f235,f231,f227,f223,f219])).
% 1.18/0.45 tff(f265,plain,(
% 1.18/0.45 ~spl17_6 | spl17_2 | spl17_1 | spl17_3 | ~spl17_4 | ~spl17_5 | ~spl17_8),
% 1.18/0.45 inference(avatar_split_clause,[],[f201,f253,f235,f231,f227,f219,f223,f239])).
% 1.18/0.45 tff(f268,plain,(
% 1.18/0.45 spl17_1 | spl17_6 | ~spl17_2),
% 1.18/0.45 inference(avatar_split_clause,[],[f198,f223,f239,f219])).
% 1.18/0.45 tff(f270,definition,(
% 1.18/0.45 spl17_9 <=> sK10 = tb2t(cons(int,t2tb1(sK11),t2tb(sK12)))),
% 1.18/0.45 introduced(definition,[new_symbols(definition,[spl17_9])],[avatar_definition])).
% 1.18/0.45 tff(f272,plain,(
% 1.18/0.45 sK10 = tb2t(cons(int,t2tb1(sK11),t2tb(sK12))) | ~spl17_9),
% 1.18/0.45 inference(avatar_component_clause,[],[f270])).
% 1.18/0.45 tff(f273,plain,(
% 1.18/0.45 ~spl17_6 | spl17_9),
% 1.18/0.45 inference(avatar_split_clause,[],[f197,f270,f239])).
% 1.18/0.45 tff(f274,plain,(
% 1.18/0.45 spl17_1 | spl17_9),
% 1.18/0.45 inference(avatar_split_clause,[],[f175,f270,f219])).
% 1.18/0.45 tff(f278,plain,(
% 1.18/0.45 t2tb(sK10) = cons(int,t2tb1(sK11),t2tb(sK12)) | ~spl17_9),
% 1.18/0.45 inference(superposition,[],[f115,f272])).
% 1.18/0.45 tff(f281,plain,(
% 1.18/0.45 ( ! [X0 : uni] : (sort1(int,X0)) )),
% 1.18/0.45 inference(superposition,[],[f117,f119])).
% 1.18/0.45 tff(f307,plain,(
% 1.18/0.45 nil(int) != t2tb(sK10) | ~spl17_9),
% 1.18/0.45 inference(superposition,[],[f103,f278])).
% 1.18/0.45 tff(f329,plain,(
% 1.18/0.45 t2tb(sK12) = cons_proj_21(int,t2tb(sK10)) | ~spl17_9),
% 1.18/0.45 inference(superposition,[],[f107,f278])).
% 1.18/0.45 tff(f425,plain,(
% 1.18/0.45 ~sorted1(sK10) | sorted1(sK12) | ~spl17_9),
% 1.18/0.45 inference(superposition,[],[f128,f272])).
% 1.18/0.45 tff(f426,plain,(
% 1.18/0.45 sorted1(sK12) | ~spl17_9),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f425,f176])).
% 1.18/0.45 tff(f434,plain,(
% 1.18/0.45 spl17_4 | ~spl17_9),
% 1.18/0.45 inference(avatar_split_clause,[],[f426,f270,f231])).
% 1.18/0.45 tff(f437,plain,(
% 1.18/0.45 $less(sK9,sK11) | sK9 = sK11 | spl17_7),
% 1.18/0.45 inference(resolution,[],[f245,f59])).
% 1.18/0.45 tff(f438,plain,(
% 1.18/0.45 $less(sK9,sK11) | (spl17_2 | spl17_7)),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f437,f224])).
% 1.18/0.45 tff(f449,plain,(
% 1.18/0.45 ~mem(int,t2tb1(sK11),t2tb(sK10)) | ~sort1(int,t2tb1(sK11)) | ~spl17_9),
% 1.18/0.45 inference(superposition,[],[f217,f278])).
% 1.18/0.45 tff(f450,plain,(
% 1.18/0.45 ~mem(int,t2tb1(sK11),t2tb(sK10)) | ~spl17_9),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f449,f117])).
% 1.18/0.45 tff(f686,plain,(
% 1.18/0.45 ( ! [X0 : uni] : (~mem(int,X0,t2tb(sK10)) | ~sort1(int,t2tb1(sK11)) | mem(int,X0,t2tb(sK12)) | ~sort1(int,X0)) ) | ~spl17_9),
% 1.18/0.45 inference(superposition,[],[f183,f278])).
% 1.18/0.45 tff(f689,plain,(
% 1.18/0.45 ( ! [X0 : uni] : (~mem(int,X0,t2tb(sK10)) | mem(int,X0,t2tb(sK12)) | ~sort1(int,X0)) ) | ~spl17_9),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f686,f117])).
% 1.18/0.45 tff(f690,plain,(
% 1.18/0.45 ( ! [X0 : uni] : (~mem(int,X0,t2tb(sK10)) | mem(int,X0,t2tb(sK12))) ) | ~spl17_9),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f689,f281])).
% 1.18/0.45 tff(f739,plain,(
% 1.18/0.45 ( ! [X0 : $int] : (~sorted1(sK10) | ~$less(X0,sK11) | mem(int,t2tb1(X0),cons(int,t2tb1(sK11),t2tb(sK12)))) ) | ~spl17_9),
% 1.18/0.45 inference(superposition,[],[f196,f272])).
% 1.18/0.45 tff(f740,plain,(
% 1.18/0.45 ( ! [X0 : $int] : (~$less(X0,sK11) | mem(int,t2tb1(X0),cons(int,t2tb1(sK11),t2tb(sK12)))) ) | ~spl17_9),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f739,f176])).
% 1.18/0.45 tff(f742,plain,(
% 1.18/0.45 ( ! [X0 : $int] : (~$less(X0,sK11) | mem(int,t2tb1(X0),t2tb(sK10))) ) | ~spl17_9),
% 1.18/0.45 inference(forward_demodulation,[],[f740,f278])).
% 1.18/0.45 tff(f788,plain,(
% 1.18/0.45 nil(int) = t2tb(sK10) | ~spl17_1),
% 1.18/0.45 inference(superposition,[],[f115,f221])).
% 1.18/0.45 tff(f793,plain,(
% 1.18/0.45 ( ! [X0 : uni] : (mem(int,X0,t2tb(sK10)) | ~sort1(int,X0)) ) | ~spl17_1),
% 1.18/0.45 inference(superposition,[],[f181,f788])).
% 1.18/0.45 tff(f798,plain,(
% 1.18/0.45 ( ! [X0 : uni] : (mem(int,X0,t2tb(sK10))) ) | ~spl17_1),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f793,f281])).
% 1.18/0.45 tff(f800,plain,(
% 1.18/0.45 $false | (~spl17_1 | spl17_6)),
% 1.18/0.45 inference(backward_subsumption_resolution,[],[f241,f798])).
% 1.18/0.45 tff(f806,plain,(
% 1.18/0.45 ~spl17_1 | spl17_6),
% 1.18/0.45 inference(avatar_contradiction_clause,[],[f800])).
% 1.18/0.45 tff(f865,plain,(
% 1.18/0.45 mem(int,t2tb1(sK9),t2tb(sK10)) | (spl17_2 | spl17_7 | ~spl17_9)),
% 1.18/0.45 inference(resolution,[],[f742,f438])).
% 1.18/0.45 tff(f866,plain,(
% 1.18/0.45 $false | (spl17_2 | spl17_6 | spl17_7 | ~spl17_9)),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f865,f241])).
% 1.18/0.45 tff(f867,plain,(
% 1.18/0.45 spl17_2 | spl17_6 | spl17_7 | ~spl17_9),
% 1.18/0.45 inference(avatar_contradiction_clause,[],[f866])).
% 1.18/0.45 tff(f955,plain,(
% 1.18/0.45 ~mem(int,t2tb1(sK9),t2tb(sK10)) | (~spl17_2 | ~spl17_9)),
% 1.18/0.45 inference(forward_demodulation,[],[f450,f225])).
% 1.18/0.45 tff(f956,plain,(
% 1.18/0.45 $false | (~spl17_2 | ~spl17_6 | ~spl17_9)),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f955,f240])).
% 1.18/0.45 tff(f957,plain,(
% 1.18/0.45 ~spl17_2 | ~spl17_6 | ~spl17_9),
% 1.18/0.45 inference(avatar_contradiction_clause,[],[f956])).
% 1.18/0.45 tff(f959,plain,(
% 1.18/0.45 $false | (~spl17_1 | ~spl17_9)),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f788,f307])).
% 1.18/0.45 tff(f960,plain,(
% 1.18/0.45 ~spl17_1 | ~spl17_9),
% 1.18/0.45 inference(avatar_contradiction_clause,[],[f959])).
% 1.18/0.45 tff(f5057,plain,(
% 1.18/0.45 mem(int,t2tb1(sK9),t2tb(sK12)) | (~spl17_6 | ~spl17_9)),
% 1.18/0.45 inference(resolution,[],[f690,f240])).
% 1.18/0.45 tff(f5065,plain,(
% 1.18/0.45 sK10 = tb2t(cons(int,t2tb1(sK14),t2tb(sK15))) | ~spl17_3),
% 1.18/0.45 inference(resolution,[],[f229,f153])).
% 1.18/0.45 tff(f5089,plain,(
% 1.18/0.45 t2tb(sK10) = cons(int,t2tb1(sK14),t2tb(sK15)) | ~spl17_3),
% 1.18/0.45 inference(superposition,[],[f115,f5065])).
% 1.18/0.45 tff(f5861,plain,(
% 1.18/0.45 spl17_8 | ~spl17_6 | ~spl17_9),
% 1.18/0.45 inference(avatar_split_clause,[],[f5057,f270,f239,f253])).
% 1.18/0.45 tff(f5864,plain,(
% 1.18/0.45 ( ! [X0 : uni] : (~sort1(int,X0) | ~sort1(int,t2tb1(sK9)) | t2tb1(sK9) = X0 | mem(int,t2tb1(sK9),cons(int,X0,t2tb(sK12)))) ) | ~spl17_8),
% 1.18/0.45 inference(resolution,[],[f255,f184])).
% 1.18/0.45 tff(f5866,plain,(
% 1.18/0.45 ( ! [X0 : uni] : (~sort1(int,X0) | t2tb1(sK9) = X0 | mem(int,t2tb1(sK9),cons(int,X0,t2tb(sK12)))) ) | ~spl17_8),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f5864,f117])).
% 1.18/0.45 tff(f5867,plain,(
% 1.18/0.45 ( ! [X0 : uni] : (mem(int,t2tb1(sK9),cons(int,X0,t2tb(sK12))) | t2tb1(sK9) = X0) ) | ~spl17_8),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f5866,f281])).
% 1.18/0.45 tff(f5874,plain,(
% 1.18/0.45 mem(int,t2tb1(sK9),t2tb(sK10)) | t2tb1(sK9) = t2tb1(sK11) | (~spl17_8 | ~spl17_9)),
% 1.18/0.45 inference(superposition,[],[f5867,f278])).
% 1.18/0.45 tff(f6047,plain,(
% 1.18/0.45 cons_proj_21(int,t2tb(sK10)) = t2tb(sK15) | ~spl17_3),
% 1.18/0.45 inference(superposition,[],[f107,f5089])).
% 1.18/0.45 tff(f6072,plain,(
% 1.18/0.45 t2tb(sK12) = t2tb(sK15) | (~spl17_3 | ~spl17_9)),
% 1.18/0.45 inference(forward_demodulation,[],[f6047,f329])).
% 1.18/0.45 tff(f6113,plain,(
% 1.18/0.45 sK15 = tb2t(t2tb(sK12)) | (~spl17_3 | ~spl17_9)),
% 1.18/0.45 inference(superposition,[],[f114,f6072])).
% 1.18/0.45 tff(f6153,plain,(
% 1.18/0.45 sK12 = sK15 | (~spl17_3 | ~spl17_9)),
% 1.18/0.45 inference(forward_demodulation,[],[f6113,f114])).
% 1.18/0.45 tff(f6157,plain,(
% 1.18/0.45 sP16(sK12,sK14,sK12,sK10) | (~spl17_3 | ~spl17_9)),
% 1.18/0.45 inference(superposition,[],[f229,f6153])).
% 1.18/0.45 tff(f6158,plain,(
% 1.18/0.45 $false | (~spl17_3 | ~spl17_9)),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f6157,f180])).
% 1.18/0.45 tff(f6159,plain,(
% 1.18/0.45 ~spl17_3 | ~spl17_9),
% 1.18/0.45 inference(avatar_contradiction_clause,[],[f6158])).
% 1.18/0.45 tff(f6161,definition,(
% 1.18/0.45 spl17_79 <=> t2tb1(sK9) = t2tb1(sK11)),
% 1.18/0.45 introduced(definition,[new_symbols(definition,[spl17_79])],[avatar_definition])).
% 1.18/0.45 tff(f6163,plain,(
% 1.18/0.45 t2tb1(sK9) = t2tb1(sK11) | ~spl17_79),
% 1.18/0.45 inference(avatar_component_clause,[],[f6161])).
% 1.18/0.45 tff(f6164,plain,(
% 1.18/0.45 spl17_79 | spl17_6 | ~spl17_8 | ~spl17_9),
% 1.18/0.45 inference(avatar_split_clause,[],[f5874,f270,f253,f239,f6161])).
% 1.18/0.45 tff(f6176,plain,(
% 1.18/0.45 sK11 = tb2t1(t2tb1(sK9)) | ~spl17_79),
% 1.18/0.45 inference(superposition,[],[f118,f6163])).
% 1.18/0.45 tff(f6197,plain,(
% 1.18/0.45 sK9 = sK11 | ~spl17_79),
% 1.18/0.45 inference(forward_demodulation,[],[f6176,f118])).
% 1.18/0.45 tff(f6199,plain,(
% 1.18/0.45 $false | (spl17_2 | ~spl17_79)),
% 1.18/0.45 inference(forward_subsumption_resolution,[],[f6197,f224])).
% 1.18/0.45 tff(f6200,plain,(
% 1.18/0.45 spl17_2 | ~spl17_79),
% 1.18/0.45 inference(avatar_contradiction_clause,[],[f6199])).
% 1.18/0.45 cnf(s4, plain, spl17_1 | spl17_3 | ~spl17_4 | ~spl17_5 | spl17_6 | ~spl17_7, inference(sat_conversion,[],[f249])).
% 1.18/0.45 cnf(s6, plain, spl17_1 | spl17_2 | spl17_3 | ~spl17_4 | spl17_5 | ~spl17_6, inference(sat_conversion,[],[f251])).
% 1.18/0.45 cnf(s7, plain, spl17_1 | spl17_2 | spl17_3 | ~spl17_4 | spl17_5 | ~spl17_7 | spl17_8, inference(sat_conversion,[],[f256])).
% 1.18/0.45 cnf(s16, plain, spl17_1 | spl17_2 | spl17_3 | ~spl17_4 | ~spl17_5 | ~spl17_6 | ~spl17_8, inference(sat_conversion,[],[f265])).
% 1.18/0.45 cnf(s19, plain, spl17_1 | ~spl17_2 | spl17_6, inference(sat_conversion,[],[f268])).
% 1.18/0.45 cnf(s20, plain, ~spl17_6 | spl17_9, inference(sat_conversion,[],[f273])).
% 1.18/0.45 cnf(s21, plain, spl17_1 | spl17_9, inference(sat_conversion,[],[f274])).
% 1.18/0.45 cnf(s24, plain, spl17_4 | ~spl17_9, inference(sat_conversion,[],[f434])).
% 1.18/0.45 cnf(s28, plain, ~spl17_1 | spl17_6, inference(sat_conversion,[],[f806])).
% 1.18/0.45 cnf(s33, plain, spl17_2 | spl17_6 | spl17_7 | ~spl17_9, inference(sat_conversion,[],[f867])).
% 1.18/0.45 cnf(s36, plain, ~spl17_2 | ~spl17_6 | ~spl17_9, inference(sat_conversion,[],[f957])).
% 1.18/0.45 cnf(s37, plain, ~spl17_1 | ~spl17_9, inference(sat_conversion,[],[f960])).
% 1.18/0.45 cnf(s140, plain, ~spl17_6 | spl17_8 | ~spl17_9, inference(sat_conversion,[],[f5861])).
% 1.18/0.45 cnf(s148, plain, ~spl17_3 | ~spl17_9, inference(sat_conversion,[],[f6159])).
% 1.18/0.45 cnf(s149, plain, spl17_6 | ~spl17_8 | ~spl17_9 | spl17_79, inference(sat_conversion,[],[f6164])).
% 1.18/0.45 cnf(s151, plain, spl17_2 | ~spl17_79, inference(sat_conversion,[],[f6200])).
% 1.18/0.45 cnf(s153, plain, spl17_5 | spl17_2 | spl17_1, inference(rat,[],[s7,s33,s149,s6,s148,s24,s21,s151])).
% 1.18/0.45 cnf(s154, plain, spl17_6 | spl17_2 | spl17_1, inference(rat,[],[s33,s4,s148,s24,s21,s153])).
% 1.18/0.45 cnf(s155, plain, spl17_2 | spl17_1, inference(rat,[],[s16,s140,s154,s153,s148,s24,s21])).
% 1.18/0.45 cnf(s156, plain, spl17_1, inference(rat,[],[s36,s19,s155,s21])).
% 1.18/0.45 cnf(s157, plain, ~spl17_9, inference(rat,[],[s37,s156])).
% 1.18/0.45 cnf(s158, plain, spl17_6, inference(rat,[],[s28,s156])).
% 1.18/0.45 cnf(s159, plain, $false, inference(rat,[],[s20,s157,s158])).
% 1.18/0.45 tff(f6201,plain,(
% 1.18/0.45 $false),
% 1.18/0.45 inference(avatar_sat_refutation,[],[s159])).
% 1.18/0.45 % SZS output end Proof for theBenchmark
% 1.18/0.45 % (383393)------------------------------
% 1.18/0.45 % (383393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.18/0.45 % (383393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.18/0.45 % (383393)CaDiCaL version: 2.1.3
% 1.18/0.45 % (383393)Termination reason: Refutation
% 1.18/0.45 % (383393)Time elapsed: 0.196 s
% 1.18/0.45 % (383393)Peak memory usage: 15 MB
% 1.18/0.45 % (383393)Instructions burned: 312 (million)
% 1.18/0.45 % (383387)Success in time 0.234 s
% 1.18/0.45 % Vampire exiting
%------------------------------------------------------------------------------