%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COM172^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 : Wed Sep 30 07:46:23 AM UTC 2026
% Result : Theorem 2.91s 0.85s
% Output : Refutation 2.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM172^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n014.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 17:47:15 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running higher-order theorem proving
% 0.21/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.52/0.43 % (2988074)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.52/0.43 % (2988083)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3049258621:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.52/0.43 % (2988085)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.52/0.43 % (2988085)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.52/0.43 % (2988083)Instruction limit reached!
% 0.52/0.43 % (2988083)------------------------------
% 0.52/0.43 % (2988083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.43 % (2988083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.43 % (2988083)CaDiCaL version: 2.1.3
% 0.52/0.43 % (2988083)Termination reason: Instruction limit
% 0.52/0.43 % (2988083)Termination phase: Property scanning
% 0.52/0.43 % (2988083)Time elapsed: 0.007 s
% 0.52/0.43 % (2988083)Peak memory usage: 10 MB
% 0.52/0.43 % (2988083)Instructions burned: 27 (million)
% 0.52/0.43 % (2988079)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3527551646:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.52/0.43 % (2988081)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=487942258:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.52/0.43 % (2988082)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=1263920731:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.52/0.43 % (2988084)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2766679158:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.52/0.43 % (2988085)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=610368937:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.52/0.43 % (2988081)Instruction limit reached!
% 0.52/0.43 % (2988081)------------------------------
% 0.52/0.43 % (2988081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.43 % (2988081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.43 % (2988081)CaDiCaL version: 2.1.3
% 0.52/0.43 % (2988081)Termination reason: Instruction limit
% 0.52/0.43 % (2988081)Termination phase: shuffling
% 0.52/0.43 % (2988081)Time elapsed: 0.002 s
% 0.52/0.43 % (2988081)Peak memory usage: 10 MB
% 0.52/0.43 % (2988081)Instructions burned: 3 (million)
% 0.52/0.43 % (2988089)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2634350840:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.52/0.43 % (2988080)lrs+10_16_si=on:nwc=1.5:random_seed=3908671356:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.52/0.43 % (2988089)Instruction limit reached!
% 0.52/0.43 % (2988089)------------------------------
% 0.52/0.43 % (2988089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.43 % (2988089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.43 % (2988089)CaDiCaL version: 2.1.3
% 0.52/0.43 % (2988089)Termination reason: Instruction limit
% 0.52/0.43 % (2988089)Termination phase: shuffling
% 0.52/0.43 % (2988089)Time elapsed: 0.001 s
% 0.52/0.43 % (2988089)Peak memory usage: 10 MB
% 0.52/0.43 % (2988089)Instructions burned: 6 (million)
% 0.52/0.43 % (2988096)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.52/0.43 % (2988093)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1189883949:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.52/0.43 % (2988096)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2297347088:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.52/0.43 % (2988096)Instruction limit reached!
% 0.52/0.43 % (2988096)------------------------------
% 0.52/0.43 % (2988096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.47 % (2988096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.47 % (2988096)CaDiCaL version: 2.1.3
% 0.52/0.47 % (2988096)Termination reason: Instruction limit
% 0.52/0.47 % (2988096)Termination phase: shuffling
% 0.52/0.47 % (2988096)Time elapsed: 0.002 s
% 0.52/0.47 % (2988096)Peak memory usage: 10 MB
% 0.52/0.47 % (2988096)Instructions burned: 9 (million)
% 0.52/0.47 % (2988093)Instruction limit reached!
% 0.52/0.47 % (2988093)------------------------------
% 0.52/0.47 % (2988093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.47 % (2988093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.47 % (2988093)CaDiCaL version: 2.1.3
% 0.52/0.47 % (2988093)Termination reason: Instruction limit
% 0.52/0.47 % (2988093)Termination phase: shuffling
% 0.52/0.47 % (2988093)Time elapsed: 0.003 s
% 0.52/0.47 % (2988093)Peak memory usage: 10 MB
% 0.52/0.47 % (2988093)Instructions burned: 6 (million)
% 0.52/0.47 % (2988080)Instruction limit reached!
% 0.52/0.47 % (2988080)------------------------------
% 0.52/0.47 % (2988080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.47 % (2988080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.47 % (2988080)CaDiCaL version: 2.1.3
% 0.52/0.47 % (2988080)Termination reason: Instruction limit
% 0.52/0.47 % (2988080)Termination phase: shuffling
% 0.52/0.47 % (2988080)Time elapsed: 0.021 s
% 0.52/0.47 % (2988080)Peak memory usage: 10 MB
% 0.52/0.47 % (2988080)Instructions burned: 20 (million)
% 0.52/0.47 % (2988099)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3548842434:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.52/0.47 % (2988084)Instruction limit reached!
% 0.52/0.47 % (2988084)------------------------------
% 0.52/0.47 % (2988084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.47 % (2988084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.47 % (2988084)CaDiCaL version: 2.1.3
% 0.52/0.47 % (2988084)Termination reason: Instruction limit
% 0.52/0.47 % (2988084)Termination phase: Property scanning
% 0.52/0.47 % (2988084)Time elapsed: 0.037 s
% 0.52/0.47 % (2988084)Peak memory usage: 12 MB
% 0.52/0.47 % (2988084)Instructions burned: 76 (million)
% 0.52/0.47 % (2988100)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.52/0.47 % (2988100)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.52/0.47 % (2988079)Instruction limit reached!
% 0.52/0.47 % (2988079)------------------------------
% 0.52/0.47 % (2988079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.47 % (2988079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.47 % (2988079)CaDiCaL version: 2.1.3
% 0.52/0.47 % (2988079)Termination reason: Instruction limit
% 0.52/0.47 % (2988079)Termination phase: Function definition elimination
% 0.52/0.47 % (2988079)Time elapsed: 0.042 s
% 0.52/0.47 % (2988079)Peak memory usage: 12 MB
% 0.52/0.47 % (2988079)Instructions burned: 89 (million)
% 0.52/0.47 % (2988100)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2377512373:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.52/0.47 % (2988101)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=2533295534:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.52/0.47 % (2988099)Instruction limit reached!
% 0.52/0.47 % (2988099)------------------------------
% 0.52/0.47 % (2988099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.47 % (2988099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.47 % (2988099)CaDiCaL version: 2.1.3
% 0.52/0.47 % (2988099)Termination reason: Instruction limit
% 0.52/0.47 % (2988099)Termination phase: shuffling
% 0.52/0.47 % (2988099)Time elapsed: 0.014 s
% 0.52/0.47 % (2988099)Peak memory usage: 10 MB
% 0.52/0.47 % (2988099)Instructions burned: 12 (million)
% 0.52/0.47 % (2988103)lrs+10_1_si=on:cs=on:random_seed=1039807767:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.31/0.51 % (2988104)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.31/0.51 % (2988100)Instruction limit reached!
% 1.31/0.51 % (2988100)------------------------------
% 1.31/0.51 % (2988100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.51 % (2988100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.51 % (2988100)CaDiCaL version: 2.1.3
% 1.31/0.51 % (2988100)Termination reason: Instruction limit
% 1.31/0.51 % (2988100)Termination phase: shuffling
% 1.31/0.51 % (2988100)Time elapsed: 0.014 s
% 1.31/0.51 % (2988100)Peak memory usage: 10 MB
% 1.31/0.51 % (2988100)Instructions burned: 30 (million)
% 1.31/0.51 % (2988103)Instruction limit reached!
% 1.31/0.51 % (2988103)------------------------------
% 1.31/0.51 % (2988103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.51 % (2988103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.51 % (2988103)CaDiCaL version: 2.1.3
% 1.31/0.51 % (2988103)Termination reason: Instruction limit
% 1.31/0.51 % (2988103)Termination phase: shuffling
% 1.31/0.51 % (2988103)Time elapsed: 0.005 s
% 1.31/0.51 % (2988103)Peak memory usage: 10 MB
% 1.31/0.51 % (2988103)Instructions burned: 9 (million)
% 1.31/0.51 % (2988104)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=3578954334:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.31/0.51 % (2988104)Instruction limit reached!
% 1.31/0.51 % (2988104)------------------------------
% 1.31/0.51 % (2988104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.51 % (2988104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.51 % (2988104)CaDiCaL version: 2.1.3
% 1.31/0.51 % (2988104)Termination reason: Instruction limit
% 1.31/0.51 % (2988104)Termination phase: shuffling
% 1.31/0.51 % (2988104)Time elapsed: 0.003 s
% 1.31/0.51 % (2988104)Peak memory usage: 10 MB
% 1.31/0.51 % (2988104)Instructions burned: 5 (million)
% 1.31/0.51 % (2988101)Instruction limit reached!
% 1.31/0.51 % (2988101)------------------------------
% 1.31/0.51 % (2988101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.51 % (2988101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.51 % (2988101)CaDiCaL version: 2.1.3
% 1.31/0.51 % (2988101)Termination reason: Instruction limit
% 1.31/0.51 % (2988101)Termination phase: Preprocessing 3
% 1.31/0.51 % (2988101)Time elapsed: 0.020 s
% 1.31/0.51 % (2988101)Peak memory usage: 11 MB
% 1.31/0.51 % (2988101)Instructions burned: 89 (million)
% 1.31/0.51 % (2988107)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2995417918:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.31/0.51 % (2988113)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1889778938:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.31/0.51 % (2988109)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1249199062:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.31/0.51 % (2988085)Instruction limit reached!
% 1.31/0.51 % (2988085)------------------------------
% 1.31/0.51 % (2988085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.51 % (2988085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.51 % (2988085)CaDiCaL version: 2.1.3
% 1.31/0.51 % (2988085)Termination reason: Instruction limit
% 1.31/0.51 % (2988085)Termination phase: Saturation
% 1.31/0.51 % (2988085)Time elapsed: 0.077 s
% 1.31/0.51 % (2988085)Peak memory usage: 14 MB
% 1.31/0.51 % (2988085)Instructions burned: 157 (million)
% 1.31/0.51 % (2988110)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1291801731:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.31/0.51 % (2988112)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2053151438:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.31/0.51 % (2988107)Instruction limit reached!
% 1.31/0.51 % (2988107)------------------------------
% 1.31/0.51 % (2988107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.51 % (2988107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.56 % (2988107)CaDiCaL version: 2.1.3
% 1.31/0.56 % (2988107)Termination reason: Instruction limit
% 1.31/0.56 % (2988107)Termination phase: SInE selection
% 1.31/0.56 % (2988107)Time elapsed: 0.018 s
% 1.31/0.56 % (2988107)Peak memory usage: 11 MB
% 1.31/0.56 % (2988107)Instructions burned: 38 (million)
% 1.31/0.56 % (2988112)Instruction limit reached!
% 1.31/0.56 % (2988112)------------------------------
% 1.31/0.56 % (2988112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.56 % (2988112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.56 % (2988112)CaDiCaL version: 2.1.3
% 1.31/0.56 % (2988112)Termination reason: Instruction limit
% 1.31/0.56 % (2988112)Termination phase: shuffling
% 1.31/0.56 % (2988112)Time elapsed: 0.007 s
% 1.31/0.56 % (2988112)Peak memory usage: 10 MB
% 1.31/0.56 % (2988112)Instructions burned: 15 (million)
% 1.31/0.56 % (2988110)Instruction limit reached!
% 1.31/0.56 % (2988110)------------------------------
% 1.31/0.56 % (2988110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.56 % (2988110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.56 % (2988110)CaDiCaL version: 2.1.3
% 1.31/0.56 % (2988110)Termination reason: Instruction limit
% 1.31/0.56 % (2988110)Termination phase: Property scanning
% 1.31/0.56 % (2988110)Time elapsed: 0.012 s
% 1.31/0.56 % (2988110)Peak memory usage: 10 MB
% 1.31/0.56 % (2988110)Instructions burned: 26 (million)
% 1.31/0.56 % (2988117)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3501285704:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.31/0.56 % (2988117)Instruction limit reached!
% 1.31/0.56 % (2988117)------------------------------
% 1.31/0.56 % (2988117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.56 % (2988117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.56 % (2988117)CaDiCaL version: 2.1.3
% 1.31/0.56 % (2988117)Termination reason: Instruction limit
% 1.31/0.56 % (2988117)Termination phase: shuffling
% 1.31/0.56 % (2988117)Time elapsed: 0.007 s
% 1.31/0.56 % (2988117)Peak memory usage: 10 MB
% 1.31/0.56 % (2988117)Instructions burned: 14 (million)
% 1.31/0.56 % (2988120)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2826226431:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.31/0.56 % (2988120)Instruction limit reached!
% 1.31/0.56 % (2988120)------------------------------
% 1.31/0.56 % (2988120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.56 % (2988120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.56 % (2988120)CaDiCaL version: 2.1.3
% 1.31/0.56 % (2988120)Termination reason: Instruction limit
% 1.31/0.56 % (2988120)Termination phase: shuffling
% 1.31/0.56 % (2988120)Time elapsed: 0.002 s
% 1.31/0.56 % (2988120)Peak memory usage: 10 MB
% 1.31/0.56 % (2988120)Instructions burned: 3 (million)
% 1.31/0.56 % (2988121)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=4212481470:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.31/0.56 % (2988122)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1117039930:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.31/0.56 % (2988126)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.31/0.56 % (2988126)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.31/0.56 % (2988122)Instruction limit reached!
% 1.31/0.56 % (2988122)------------------------------
% 1.31/0.56 % (2988122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.56 % (2988122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.56 % (2988122)CaDiCaL version: 2.1.3
% 1.31/0.56 % (2988122)Termination reason: Instruction limit
% 1.31/0.56 % (2988122)Termination phase: Property scanning
% 1.31/0.56 % (2988122)Time elapsed: 0.014 s
% 1.31/0.56 % (2988122)Peak memory usage: 10 MB
% 1.31/0.56 % (2988122)Instructions burned: 30 (million)
% 1.31/0.56 % (2988126)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=3927405635:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.20/0.65 % (2988125)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3015789004:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 2.20/0.65 % (2988121)Instruction limit reached!
% 2.20/0.65 % (2988121)------------------------------
% 2.20/0.65 % (2988121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.20/0.65 % (2988121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.20/0.65 % (2988121)CaDiCaL version: 2.1.3
% 2.20/0.65 % (2988121)Termination reason: Instruction limit
% 2.20/0.65 % (2988121)Termination phase: shuffling
% 2.20/0.65 % (2988121)Time elapsed: 0.015 s
% 2.20/0.65 % (2988121)Peak memory usage: 10 MB
% 2.20/0.65 % (2988121)Instructions burned: 28 (million)
% 2.20/0.65 % (2988126)Instruction limit reached!
% 2.20/0.65 % (2988126)------------------------------
% 2.20/0.65 % (2988126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.20/0.65 % (2988126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.20/0.65 % (2988126)CaDiCaL version: 2.1.3
% 2.20/0.65 % (2988126)Termination reason: Instruction limit
% 2.20/0.65 % (2988126)Termination phase: shuffling
% 2.20/0.65 % (2988126)Time elapsed: 0.007 s
% 2.20/0.65 % (2988126)Peak memory usage: 10 MB
% 2.20/0.65 % (2988126)Instructions burned: 14 (million)
% 2.20/0.65 % (2988131)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.20/0.65 % (2988131)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=1278346950:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.20/0.65 % (2988132)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=1479333834:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 2.20/0.65 % (2988131)Instruction limit reached!
% 2.20/0.65 % (2988131)------------------------------
% 2.20/0.65 % (2988131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.20/0.65 % (2988131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.20/0.65 % (2988131)CaDiCaL version: 2.1.3
% 2.20/0.65 % (2988131)Termination reason: Instruction limit
% 2.20/0.65 % (2988131)Termination phase: shuffling
% 2.20/0.65 % (2988131)Time elapsed: 0.004 s
% 2.20/0.65 % (2988131)Peak memory usage: 10 MB
% 2.20/0.65 % (2988131)Instructions burned: 8 (million)
% 2.20/0.65 % (2988133)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2829389023:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 2.20/0.65 % (2988133)Instruction limit reached!
% 2.20/0.65 % (2988133)------------------------------
% 2.20/0.65 % (2988133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.20/0.65 % (2988133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.20/0.65 % (2988133)CaDiCaL version: 2.1.3
% 2.20/0.65 % (2988133)Termination reason: Instruction limit
% 2.20/0.65 % (2988133)Termination phase: shuffling
% 2.20/0.65 % (2988133)Time elapsed: 0.004 s
% 2.20/0.65 % (2988133)Peak memory usage: 10 MB
% 2.20/0.65 % (2988133)Instructions burned: 7 (million)
% 2.20/0.65 % (2988113)Instruction limit reached!
% 2.20/0.65 % (2988113)------------------------------
% 2.20/0.65 % (2988113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.20/0.65 % (2988113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.20/0.65 % (2988113)CaDiCaL version: 2.1.3
% 2.20/0.65 % (2988113)Termination reason: Instruction limit
% 2.20/0.65 % (2988113)Termination phase: Saturation
% 2.20/0.65 % (2988113)Time elapsed: 0.088 s
% 2.20/0.65 % (2988113)Peak memory usage: 14 MB
% 2.20/0.65 % (2988113)Instructions burned: 329 (million)
% 2.20/0.65 % (2988132)Instruction limit reached!
% 2.20/0.65 % (2988132)------------------------------
% 2.20/0.65 % (2988132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.20/0.65 % (2988132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.20/0.65 % (2988132)CaDiCaL version: 2.1.3
% 2.20/0.65 % (2988132)Termination reason: Instruction limit
% 2.20/0.65 % (2988132)Termination phase: shuffling
% 2.20/0.65 % (2988132)Time elapsed: 0.015 s
% 2.65/0.71 % (2988132)Peak memory usage: 10 MB
% 2.65/0.71 % (2988132)Instructions burned: 33 (million)
% 2.65/0.71 % (2988137)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=46877329:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.65/0.71 % (2988139)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=394967804:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.65/0.71 % (2988138)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1119029661:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.65/0.71 % (2988125)Instruction limit reached!
% 2.65/0.71 % (2988125)------------------------------
% 2.65/0.71 % (2988125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.71 % (2988125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.71 % (2988125)CaDiCaL version: 2.1.3
% 2.65/0.71 % (2988125)Termination reason: Instruction limit
% 2.65/0.71 % (2988125)Termination phase: Clausification
% 2.65/0.71 % (2988125)Time elapsed: 0.051 s
% 2.65/0.71 % (2988125)Peak memory usage: 12 MB
% 2.65/0.71 % (2988125)Instructions burned: 60 (million)
% 2.65/0.71 % (2988137)Instruction limit reached!
% 2.65/0.71 % (2988137)------------------------------
% 2.65/0.71 % (2988137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.71 % (2988137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.71 % (2988137)CaDiCaL version: 2.1.3
% 2.65/0.71 % (2988137)Termination reason: Instruction limit
% 2.65/0.71 % (2988137)Termination phase: shuffling
% 2.65/0.71 % (2988137)Time elapsed: 0.011 s
% 2.65/0.71 % (2988137)Peak memory usage: 10 MB
% 2.65/0.71 % (2988137)Instructions burned: 23 (million)
% 2.65/0.71 % (2988140)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3568032792:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.65/0.71 % (2988138)Instruction limit reached!
% 2.65/0.71 % (2988138)------------------------------
% 2.65/0.71 % (2988138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.71 % (2988138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.71 % (2988138)CaDiCaL version: 2.1.3
% 2.65/0.71 % (2988138)Termination reason: Instruction limit
% 2.65/0.71 % (2988138)Termination phase: shuffling
% 2.65/0.71 % (2988138)Time elapsed: 0.010 s
% 2.65/0.71 % (2988138)Peak memory usage: 10 MB
% 2.65/0.71 % (2988138)Instructions burned: 20 (million)
% 2.65/0.71 % (2988145)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2797301481:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.65/0.71 % (2988147)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.65/0.71 % (2988147)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1496449862:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.65/0.71 % (2988144)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3490060966:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.65/0.71 % (2988147)Instruction limit reached!
% 2.65/0.71 % (2988147)------------------------------
% 2.65/0.71 % (2988147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.71 % (2988147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.71 % (2988147)CaDiCaL version: 2.1.3
% 2.65/0.71 % (2988147)Termination reason: Instruction limit
% 2.65/0.71 % (2988147)Termination phase: shuffling
% 2.65/0.71 % (2988147)Time elapsed: 0.004 s
% 2.65/0.71 % (2988147)Peak memory usage: 10 MB
% 2.65/0.71 % (2988147)Instructions burned: 7 (million)
% 2.65/0.71 % (2988109)Instruction limit reached!
% 2.65/0.71 % (2988109)------------------------------
% 2.65/0.71 % (2988109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.71 % (2988109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.71 % (2988109)CaDiCaL version: 2.1.3
% 2.65/0.71 % (2988109)Termination reason: Instruction limit
% 2.65/0.71 % (2988109)Termination phase: Saturation
% 2.65/0.71 % (2988109)Time elapsed: 0.132 s
% 2.65/0.71 % (2988109)Peak memory usage: 14 MB
% 2.65/0.71 % (2988109)Instructions burned: 250 (million)
% 2.65/0.71 % (2988145)Instruction limit reached!
% 2.65/0.71 % (2988145)------------------------------
% 2.91/0.81 % (2988145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.81 % (2988145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.81 % (2988145)CaDiCaL version: 2.1.3
% 2.91/0.81 % (2988145)Termination reason: Instruction limit
% 2.91/0.81 % (2988145)Termination phase: Preprocessing 2
% 2.91/0.81 % (2988145)Time elapsed: 0.020 s
% 2.91/0.81 % (2988145)Peak memory usage: 11 MB
% 2.91/0.81 % (2988145)Instructions burned: 43 (million)
% 2.91/0.81 % (2988151)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2244137076:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.91/0.81 % (2988152)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=3894993750:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.91/0.81 % (2988153)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.91/0.81 % (2988140)Instruction limit reached!
% 2.91/0.81 % (2988140)------------------------------
% 2.91/0.81 % (2988140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.81 % (2988140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.81 % (2988140)CaDiCaL version: 2.1.3
% 2.91/0.81 % (2988140)Termination reason: Instruction limit
% 2.91/0.81 % (2988140)Termination phase: Saturation
% 2.91/0.81 % (2988140)Time elapsed: 0.068 s
% 2.91/0.81 % (2988140)Peak memory usage: 13 MB
% 2.91/0.81 % (2988140)Instructions burned: 144 (million)
% 2.91/0.81 % (2988153)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=4125351175:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.91/0.81 % (2988153)Instruction limit reached!
% 2.91/0.81 % (2988153)------------------------------
% 2.91/0.81 % (2988153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.81 % (2988153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.81 % (2988153)CaDiCaL version: 2.1.3
% 2.91/0.81 % (2988153)Termination reason: Instruction limit
% 2.91/0.81 % (2988153)Termination phase: shuffling
% 2.91/0.81 % (2988153)Time elapsed: 0.006 s
% 2.91/0.81 % (2988153)Peak memory usage: 10 MB
% 2.91/0.81 % (2988153)Instructions burned: 7 (million)
% 2.91/0.81 % (2988157)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2193856520:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 2.91/0.81 % (2988158)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2189775203:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 2.91/0.81 % (2988157)Instruction limit reached!
% 2.91/0.81 % (2988157)------------------------------
% 2.91/0.81 % (2988157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.81 % (2988157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.81 % (2988157)CaDiCaL version: 2.1.3
% 2.91/0.81 % (2988157)Termination reason: Instruction limit
% 2.91/0.81 % (2988157)Termination phase: shuffling
% 2.91/0.81 % (2988157)Time elapsed: 0.011 s
% 2.91/0.81 % (2988157)Peak memory usage: 10 MB
% 2.91/0.81 % (2988157)Instructions burned: 22 (million)
% 2.91/0.81 % (2988158)Instruction limit reached!
% 2.91/0.81 % (2988158)------------------------------
% 2.91/0.81 % (2988158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.81 % (2988158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.81 % (2988158)CaDiCaL version: 2.1.3
% 2.91/0.81 % (2988158)Termination reason: Instruction limit
% 2.91/0.81 % (2988158)Termination phase: shuffling
% 2.91/0.81 % (2988158)Time elapsed: 0.010 s
% 2.91/0.81 % (2988158)Peak memory usage: 10 MB
% 2.91/0.81 % (2988158)Instructions burned: 21 (million)
% 2.91/0.81 % (2988161)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=2321794483:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 2.91/0.81 % (2988162)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=2781422995:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 2.91/0.85 % (2988152)Instruction limit reached!
% 2.91/0.85 % (2988152)------------------------------
% 2.91/0.85 % (2988152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988152)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988152)Termination reason: Instruction limit
% 2.91/0.85 % (2988152)Termination phase: Saturation
% 2.91/0.85 % (2988152)Time elapsed: 0.086 s
% 2.91/0.85 % (2988152)Peak memory usage: 14 MB
% 2.91/0.85 % (2988152)Instructions burned: 171 (million)
% 2.91/0.85 % (2988144)Instruction limit reached!
% 2.91/0.85 % (2988144)------------------------------
% 2.91/0.85 % (2988144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988144)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988144)Termination reason: Instruction limit
% 2.91/0.85 % (2988144)Termination phase: Saturation
% 2.91/0.85 % (2988144)Time elapsed: 0.116 s
% 2.91/0.85 % (2988144)Peak memory usage: 14 MB
% 2.91/0.85 % (2988144)Instructions burned: 194 (million)
% 2.91/0.85 % (2988151)Instruction limit reached!
% 2.91/0.85 % (2988151)------------------------------
% 2.91/0.85 % (2988151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988151)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988151)Termination reason: Instruction limit
% 2.91/0.85 % (2988151)Termination phase: Saturation
% 2.91/0.85 % (2988151)Time elapsed: 0.100 s
% 2.91/0.85 % (2988151)Peak memory usage: 14 MB
% 2.91/0.85 % (2988151)Instructions burned: 181 (million)
% 2.91/0.85 % (2988165)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=1001479742:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 2.91/0.85 % (2988166)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1373315534:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 2.91/0.85 % (2988082)Instruction limit reached!
% 2.91/0.85 % (2988082)------------------------------
% 2.91/0.85 % (2988082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988082)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988082)Termination reason: Instruction limit
% 2.91/0.85 % (2988082)Termination phase: Saturation
% 2.91/0.85 % (2988082)Time elapsed: 0.347 s
% 2.91/0.85 % (2988082)Peak memory usage: 16 MB
% 2.91/0.85 % (2988082)Instructions burned: 635 (million)
% 2.91/0.85 % (2988167)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=4284050838:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 2.91/0.85 % (2988165)Instruction limit reached!
% 2.91/0.85 % (2988165)------------------------------
% 2.91/0.85 % (2988165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988165)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988165)Termination reason: Instruction limit
% 2.91/0.85 % (2988165)Termination phase: Property scanning
% 2.91/0.85 % (2988165)Time elapsed: 0.021 s
% 2.91/0.85 % (2988165)Peak memory usage: 10 MB
% 2.91/0.85 % (2988165)Instructions burned: 47 (million)
% 2.91/0.85 % (2988167)Instruction limit reached!
% 2.91/0.85 % (2988167)------------------------------
% 2.91/0.85 % (2988167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988167)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988167)Termination reason: Instruction limit
% 2.91/0.85 % (2988167)Termination phase: shuffling
% 2.91/0.85 % (2988167)Time elapsed: 0.010 s
% 2.91/0.85 % (2988167)Peak memory usage: 10 MB
% 2.91/0.85 % (2988167)Instructions burned: 22 (million)
% 2.91/0.85 % (2988171)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.91/0.85 % (2988171)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1702665999:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 2.91/0.85 % (2988172)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2964460053:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2995 on theBenchmark for (2995ds/13Mi)
% 2.91/0.85 % (2988173)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=3775698796:i=66:s2at=3:nm=2:rtra=on:rawr=on_2995 on theBenchmark for (2995ds/66Mi)
% 2.91/0.85 % (2988172)Instruction limit reached!
% 2.91/0.85 % (2988172)------------------------------
% 2.91/0.85 % (2988172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988172)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988172)Termination reason: Instruction limit
% 2.91/0.85 % (2988172)Termination phase: shuffling
% 2.91/0.85 % (2988172)Time elapsed: 0.007 s
% 2.91/0.85 % (2988172)Peak memory usage: 10 MB
% 2.91/0.85 % (2988172)Instructions burned: 15 (million)
% 2.91/0.85 % (2988177)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2387191384:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 2.91/0.85 % (2988173)Instruction limit reached!
% 2.91/0.85 % (2988173)------------------------------
% 2.91/0.85 % (2988173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988173)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988173)Termination reason: Instruction limit
% 2.91/0.85 % (2988173)Termination phase: SInE selection
% 2.91/0.85 % (2988173)Time elapsed: 0.029 s
% 2.91/0.85 % (2988173)Peak memory usage: 11 MB
% 2.91/0.85 % (2988173)Instructions burned: 67 (million)
% 2.91/0.85 % (2988179)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=125593546:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 2.91/0.85 % (2988177)Instruction limit reached!
% 2.91/0.85 % (2988177)------------------------------
% 2.91/0.85 % (2988177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988177)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988177)Termination reason: Instruction limit
% 2.91/0.85 % (2988177)Termination phase: Preprocessing 3
% 2.91/0.85 % (2988177)Time elapsed: 0.025 s
% 2.91/0.85 % (2988177)Peak memory usage: 11 MB
% 2.91/0.85 % (2988177)Instructions burned: 53 (million)
% 2.91/0.85 % (2988179)Instruction limit reached!
% 2.91/0.85 % (2988179)------------------------------
% 2.91/0.85 % (2988179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988179)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988179)Termination reason: Instruction limit
% 2.91/0.85 % (2988179)Termination phase: shuffling
% 2.91/0.85 % (2988179)Time elapsed: 0.014 s
% 2.91/0.85 % (2988179)Peak memory usage: 10 MB
% 2.91/0.85 % (2988179)Instructions burned: 32 (million)
% 2.91/0.85 % (2988181)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1266042438:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 2.91/0.85 % (2988139)Instruction limit reached!
% 2.91/0.85 % (2988139)------------------------------
% 2.91/0.85 % (2988139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988139)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988139)Termination reason: Instruction limit
% 2.91/0.85 % (2988139)Termination phase: Saturation
% 2.91/0.85 % (2988139)Time elapsed: 0.287 s
% 2.91/0.85 % (2988139)Peak memory usage: 16 MB
% 2.91/0.85 % (2988139)Instructions burned: 1243 (million)
% 2.91/0.85 % (2988171)Instruction limit reached!
% 2.91/0.85 % (2988171)------------------------------
% 2.91/0.85 % (2988171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988171)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988171)Termination reason: Instruction limit
% 2.91/0.85 % (2988171)Termination phase: Saturation
% 2.91/0.85 % (2988171)Time elapsed: 0.100 s
% 2.91/0.85 % (2988171)Peak memory usage: 14 MB
% 2.91/0.85 % (2988171)Instructions burned: 202 (million)
% 2.91/0.85 % (2988182)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=2887676431:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 2.91/0.85 % (2988161)Instruction limit reached!
% 2.91/0.85 % (2988161)------------------------------
% 2.91/0.85 % (2988161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988161)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988161)Termination reason: Instruction limit
% 2.91/0.85 % (2988161)Termination phase: Saturation
% 2.91/0.85 % (2988161)Time elapsed: 0.168 s
% 2.91/0.85 % (2988161)Peak memory usage: 16 MB
% 2.91/0.85 % (2988161)Instructions burned: 316 (million)
% 2.91/0.85 % (2988184)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=942886414:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2994 on theBenchmark for (2994ds/67Mi)
% 2.91/0.85 % (2988185)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 2.91/0.85 % (2988185)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1028490850:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2994 on theBenchmark for (2994ds/180Mi)
% 2.91/0.85 % (2988182)Instruction limit reached!
% 2.91/0.85 % (2988182)------------------------------
% 2.91/0.85 % (2988182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988182)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988182)Termination reason: Instruction limit
% 2.91/0.85 % (2988182)Termination phase: shuffling
% 2.91/0.85 % (2988182)Time elapsed: 0.016 s
% 2.91/0.85 % (2988182)Peak memory usage: 10 MB
% 2.91/0.85 % (2988182)Instructions burned: 35 (million)
% 2.91/0.85 % (2988187)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=570757439:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 2.91/0.85 % (2988162) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2988074-2988162"...
% 2.91/0.85 % (2988190)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=1983941154:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 2.91/0.85 % (2988162)...printing done.
% 2.91/0.85 % (2988162)Refutation found. Thanks to Tanya!
% 2.91/0.85 % SZS status Theorem for theBenchmark
% 2.91/0.85 % SZS output start Proof for theBenchmark
% 2.91/0.85 thf(type_def_5, type, coinductive_llist: $tType > $tType).
% 2.91/0.85 thf(type_def_6, type, set: $tType > $tType).
% 2.91/0.85 thf(type_def_7, type, itself: $tType > $tType).
% 2.91/0.85 thf(type_def_8, type, a: $tType).
% 2.91/0.85 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 2.91/0.85 thf(func_def_0, type, type: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.91/0.85 thf(func_def_1, type, ord: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.91/0.85 thf(func_def_2, type, order: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.91/0.85 thf(func_def_3, type, linorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.91/0.85 thf(func_def_4, type, preorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.91/0.85 thf(func_def_5, type, coindu328551480prefix: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > $o))).
% 2.91/0.85 thf(func_def_6, type, coinductive_gen_lset: !>[X0: $tType]:((set @ X0 > coinductive_llist @ X0 > set @ X0))).
% 2.91/0.85 thf(func_def_7, type, coinductive_lappend: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_8, type, coindu218763757pWhile: !>[X0: $tType]:(((X0 > $o) > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_9, type, coinductive_lfilter: !>[X0: $tType]:(((X0 > $o) > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_10, type, coinductive_lfinite: !>[X0: $tType]:((coinductive_llist @ X0 > $o))).
% 2.91/0.85 thf(func_def_11, type, coinductive_llast: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_12, type, coinductive_LCons: !>[X0: $tType]:((X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_13, type, coinductive_LNil: !>[X0: $tType]:(coinductive_llist @ X0)).
% 2.91/0.85 thf(func_def_14, type, coindu1381640503_llist: !>[X0: $tType, X1: $tType]:((X0 > (X1 > coinductive_llist @ X1 > X0) > coinductive_llist @ X1 > X0))).
% 2.91/0.85 thf(func_def_15, type, coindu1259883913_llist: !>[X0: $tType, X1: $tType]:(((X0 > $o) > (X0 > X1) > (X0 > $o) > (X0 > coinductive_llist @ X1) > (X0 > X0) > X0 > coinductive_llist @ X1))).
% 2.91/0.85 thf(func_def_16, type, coinductive_lhd: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_17, type, coinductive_lnull: !>[X0: $tType]:((coinductive_llist @ X0 > $o))).
% 2.91/0.85 thf(func_def_18, type, coinductive_lset: !>[X0: $tType]:((coinductive_llist @ X0 > set @ X0))).
% 2.91/0.85 thf(func_def_19, type, coinductive_lmember: !>[X0: $tType]:((X0 > coinductive_llist @ X0 > $o))).
% 2.91/0.85 thf(func_def_20, type, coindu1478340336prefix: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > $o))).
% 2.91/0.85 thf(func_def_21, type, coindu501562517eWhile: !>[X0: $tType]:(((X0 > $o) > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_22, type, coindu63249387sorted: !>[X0: $tType]:((coinductive_llist @ X0 > $o))).
% 2.91/0.85 thf(func_def_23, type, coindu1441602521_llist: !>[X0: $tType, X1: $tType]:(((X0 > $o) > (X0 > X1) > (X0 > X0) > X0 > coinductive_llist @ X1))).
% 2.91/0.85 thf(func_def_24, type, undefined: !>[X0: $tType]:(X0)).
% 2.91/0.85 thf(func_def_25, type, if: !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 2.91/0.85 thf(func_def_26, type, koenig916195507_paths: !>[X0: $tType]:(((X0 > X0 > $o) > set @ coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_27, type, koenig2031690877pathsp: !>[X0: $tType]:(((X0 > X0 > $o) > coinductive_llist @ X0 > $o))).
% 2.91/0.85 thf(func_def_28, type, koenig317145564le_via: !>[X0: $tType]:(((X0 > X0 > $o) > set @ X0 > X0 > set @ X0))).
% 2.91/0.85 thf(func_def_29, type, koenig1757754772e_viap: !>[X0: $tType]:(((X0 > X0 > $o) > set @ X0 > X0 > X0 > $o))).
% 2.91/0.85 thf(func_def_30, type, sup_sup: !>[X0: $tType]:((X0 > X0 > X0))).
% 2.91/0.85 thf(func_def_31, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.91/0.85 thf(func_def_32, type, type2: !>[X0: $tType]:(itself @ X0)).
% 2.91/0.85 thf(func_def_33, type, powp: !>[X0: $tType]:(((X0 > $o) > set @ X0 > $o))).
% 2.91/0.85 thf(func_def_34, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 2.91/0.85 thf(func_def_35, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 2.91/0.85 thf(func_def_36, type, graph: (a > a > $o)).
% 2.91/0.85 thf(func_def_37, type, x: coinductive_llist @ a).
% 2.91/0.85 thf(func_def_38, type, x21: a).
% 2.91/0.85 thf(func_def_39, type, x22: coinductive_llist @ a).
% 2.91/0.85 thf(func_def_40, type, xa: a).
% 2.91/0.85 thf(func_def_41, type, xs: coinductive_llist @ a).
% 2.91/0.85 thf(func_def_42, type, ys: coinductive_llist @ a).
% 2.91/0.85 thf(func_def_46, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 2.91/0.85 thf(func_def_47, type, db3: !>[X0: $tType]:(X0)).
% 2.91/0.85 thf(func_def_48, type, db0: !>[X0: $tType]:(X0)).
% 2.91/0.85 thf(func_def_49, type, db2: !>[X0: $tType]:(X0)).
% 2.91/0.85 thf(func_def_50, type, db1: !>[X0: $tType]:(X0)).
% 2.91/0.85 thf(func_def_51, type, vAND: ($o > $o > $o)).
% 2.91/0.85 thf(func_def_52, type, db5: !>[X0: $tType]:(X0)).
% 2.91/0.85 thf(func_def_53, type, db4: !>[X0: $tType]:(X0)).
% 2.91/0.85 thf(func_def_54, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.91/0.85 thf(func_def_55, type, vIMP: ($o > $o > $o)).
% 2.91/0.85 thf(func_def_56, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.91/0.85 thf(func_def_57, type, vOR: ($o > $o > $o)).
% 2.91/0.85 thf(func_def_58, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.91/0.85 thf(func_def_59, type, sK0: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_60, type, sK1: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_61, type, sK2: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_62, type, sK3: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_63, type, sK4: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_64, type, sK5: !>[X0: $tType]:(((X0 > $o) > coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_65, type, sK6: !>[X0: $tType]:(((X0 > $o) > X0 > (X0 > X0 > $o) > set @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_66, type, sK7: !>[X0: $tType]:(((X0 > $o) > X0 > (X0 > X0 > $o) > set @ X0 > X0))).
% 2.91/0.85 thf(func_def_67, type, sK8: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_68, type, sK9: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_69, type, sK10: !>[X0: $tType]:((coinductive_llist @ X0 > X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_70, type, sK11: !>[X0: $tType]:((coinductive_llist @ X0 > X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_71, type, sK12: !>[X0: $tType]:((coinductive_llist @ X0 > X0 > X0))).
% 2.91/0.85 thf(func_def_72, type, sK13: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 2.91/0.85 thf(func_def_73, type, sK14: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 2.91/0.85 thf(func_def_74, type, sK15: !>[X0: $tType]:((X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_75, type, sK16: !>[X0: $tType]:((X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_76, type, sK17: !>[X0: $tType]:(((X0 > $o) > X0 > set @ X0 > (X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_77, type, sK18: !>[X0: $tType]:(((X0 > $o) > X0 > set @ X0 > (X0 > X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_78, type, sK19: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_79, type, sK20: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_80, type, sK21: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_81, type, sK22: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_82, type, sK23: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_83, type, sK24: !>[X0: $tType]:(((X0 > X0 > $o) > X0 > set @ X0 > X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_84, type, sK25: !>[X0: $tType]:(((X0 > X0 > $o) > X0 > set @ X0 > X0 > X0))).
% 2.91/0.85 thf(func_def_85, type, sK26: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_86, type, sK27: !>[X0: $tType]:(((X0 > X0 > $o) > X0 > set @ X0 > X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_87, type, sK28: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_88, type, sK29: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_89, type, sK30: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > coinductive_llist @ X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_90, type, sK31: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > coinductive_llist @ X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_91, type, sK32: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_92, type, sK33: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_93, type, sK34: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_94, type, sK35: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_95, type, sK36: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_96, type, sK37: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_97, type, sK38: !>[X0: $tType]:(((X0 > $o) > set @ X0 > X0))).
% 2.91/0.85 thf(func_def_98, type, sK39: !>[X0: $tType]:(((X0 > $o) > coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_99, type, sK40: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 2.91/0.85 thf(func_def_100, type, sK41: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 2.91/0.85 thf(func_def_101, type, sK42: !>[X0: $tType]:((set @ X0 > set @ X0 > X0))).
% 2.91/0.85 thf(func_def_102, type, sK43: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 2.91/0.85 thf(func_def_103, type, sK44: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 2.91/0.85 thf(func_def_104, type, sK45: !>[X0: $tType]:((coinductive_llist @ X0 > X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_105, type, sK46: !>[X0: $tType]:((coinductive_llist @ X0 > X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_106, type, sK47: !>[X0: $tType]:(((X0 > $o) > coinductive_llist @ X0 > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_107, type, sK48: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > (X0 > X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_108, type, sK49: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_109, type, sK50: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_110, type, sK51: !>[X0: $tType]:((set @ X0 > (X0 > $o) > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_111, type, sK52: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > X1) > X0))).
% 2.91/0.85 thf(func_def_112, type, sK53: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > (X0 > X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_113, type, sK54: !>[X0: $tType]:(((X0 > coinductive_llist @ X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_114, type, sK55: !>[X0: $tType]:(((X0 > coinductive_llist @ X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_115, type, sK56: !>[X0: $tType]:(((X0 > coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_116, type, sK57: !>[X0: $tType]:(((X0 > coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_117, type, sK58: !>[X0: $tType]:(((X0 > coinductive_llist @ X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_118, type, sK59: !>[X0: $tType]:(((X0 > $o) > coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_119, type, sK60: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_120, type, sK61: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 2.91/0.85 thf(func_def_121, type, sK62: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 2.91/0.85 thf(func_def_122, type, sK63: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_123, type, sK64: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_124, type, sK65: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_125, type, sK66: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_126, type, sK67: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_127, type, sK68: !>[X0: $tType]:((X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_128, type, sK69: !>[X0: $tType]:((X0 > coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_129, type, sK70: !>[X0: $tType]:((X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_130, type, sK71: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > X0 > (X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_131, type, sK72: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > X0 > (X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_132, type, sK73: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_133, type, sK74: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_134, type, sK75: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_135, type, sK76: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_136, type, sK77: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_137, type, sK78: !>[X0: $tType]:(((X0 > $o) > coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_138, type, sK79: !>[X0: $tType]:((X0 > (coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_139, type, sK80: !>[X0: $tType]:((X0 > (coinductive_llist @ X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_140, type, sK81: !>[X0: $tType]:((X0 > (coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_141, type, sK82: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_142, type, sK83: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_143, type, sK84: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_144, type, sK85: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_145, type, sK86: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_146, type, sK87: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_147, type, sK88: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_148, type, sK89: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_149, type, sK90: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 2.91/0.85 thf(func_def_150, type, sK91: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_151, type, sK92: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_152, type, sK93: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_153, type, sK94: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_154, type, sK95: !>[X0: $tType]:((X0 > coinductive_llist @ X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_155, type, sK96: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_156, type, sK97: !>[X0: $tType]:((X0 > (coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_157, type, sK98: !>[X0: $tType]:((X0 > (coinductive_llist @ X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_158, type, sK99: !>[X0: $tType]:((X0 > (coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_159, type, sK100: !>[X0: $tType]:((X0 > coinductive_llist @ X0 > X0))).
% 2.91/0.85 thf(func_def_160, type, sK101: !>[X0: $tType]:((set @ X0 > X0 > (X0 > X0 > $o) > X0 > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_161, type, sK102: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_162, type, sK103: !>[X0: $tType]:((coinductive_llist @ X0 > (X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_163, type, sK104: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > X0))).
% 2.91/0.85 thf(func_def_164, type, sK105: !>[X0: $tType]:(((coinductive_llist @ X0 > $o) > coinductive_llist @ X0))).
% 2.91/0.85 thf(func_def_165, type, vNOT: ($o > $o)).
% 2.91/0.85 thf(f10,axiom,(
% 2.91/0.85 ! [X0 : $tType,X1 : coinductive_llist @ X0] : (((coinductive_lappend @ X0 @ X1 @ coinductive_LNil @ X0)) = X1)),
% 2.91/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9_lappend__LNil2)).
% 2.91/0.85 thf(f11,axiom,(
% 2.91/0.85 ! [X0 : $tType,X3 : coinductive_llist @ X0,X1 : X0,X2 : coinductive_llist @ X0] : (((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ X1 @ X2) @ X3)) = ((coinductive_LCons @ X0 @ X1 @ (coinductive_lappend @ X0 @ X2 @ X3))))),
% 2.91/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_10_lappend__code_I2_J)).
% 2.91/0.85 thf(f13,axiom,(
% 2.91/0.85 ! [X0 : $tType,X3 : X0,X4 : coinductive_llist @ X0,X2 : coinductive_llist @ X0,X1 : X0] : ((((coinductive_LCons @ X0 @ X1 @ X2)) = ((coinductive_LCons @ X0 @ X3 @ X4))) = (X1 = X3) & (X2 = X4))),
% 2.91/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_12_llist_Oinject)).
% 2.91/0.85 thf(f16,axiom,(
% 2.91/0.85 ! [X0 : $tType,X1 : coinductive_llist @ X0,X2 : coinductive_llist @ X0] : ((X1 = coinductive_LNil @ X0) & (X2 = coinductive_LNil @ X0) = (((coinductive_lappend @ X0 @ X1 @ X2)) = coinductive_LNil @ X0))),
% 2.91/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_15_lappend__eq__LNil__iff)).
% 2.91/0.85 thf(f17,axiom,(
% 2.91/0.85 ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : X0] : (coinductive_LNil @ X0 != ((coinductive_LCons @ X0 @ X1 @ X2)))),
% 2.91/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_16_llist_Odistinct_I1_J)).
% 2.91/0.85 thf(f18,axiom,(
% 2.91/0.85 ! [X0 : $tType,X1 : coinductive_llist @ X0] : ((X1 != coinductive_LNil @ X0) => ~ ! [X2 : X0,X3 : coinductive_llist @ X0] : (X1 != ((coinductive_LCons @ X0 @ X2 @ X3))))),
% 2.91/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_17_llist_Oexhaust)).
% 2.91/0.85 thf(f268,axiom,(
% 2.91/0.85 (((coinductive_lappend @ a @ x @ ys)) = ((coinductive_LCons @ a @ xa @ coinductive_LNil @ a)))),
% 2.91/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 2.91/0.85 thf(f269,axiom,(
% 2.91/0.85 (x = ((coinductive_LCons @ a @ x21 @ x22)))),
% 2.91/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1)).
% 2.91/0.85 thf(f270,conjecture,(
% 2.91/0.85 ? [X2 : coinductive_llist @ a,X0 : a,X1 : a] : (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ X1 @ X2) @ (koenig916195507_paths @ a @ graph)) | (member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ X1 @ X2) @ ys) @ (koenig916195507_paths @ a @ graph))) & (graph @ X0 @ X1) & (x = ((coinductive_LCons @ a @ X0 @ (coinductive_LCons @ a @ X1 @ X2))))) | (x = coinductive_LNil @ a) | ? [X0 : a] : (x = ((coinductive_LCons @ a @ X0 @ coinductive_LNil @ a)))),
% 2.91/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_2)).
% 2.91/0.85 thf(f271,negated_conjecture,(
% 2.91/0.85 ~(? [X2 : coinductive_llist @ a,X0 : a,X1 : a] : (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ X1 @ X2) @ (koenig916195507_paths @ a @ graph)) | (member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ X1 @ X2) @ ys) @ (koenig916195507_paths @ a @ graph))) & (graph @ X0 @ X1) & (x = ((coinductive_LCons @ a @ X0 @ (coinductive_LCons @ a @ X1 @ X2))))) | (x = coinductive_LNil @ a) | ? [X0 : a] : (x = ((coinductive_LCons @ a @ X0 @ coinductive_LNil @ a))))),
% 2.91/0.85 inference(negated_conjecture,[status(cth)],[f270])).
% 2.91/0.85 thf(f385,plain,(
% 2.91/0.85 ~(? [X0 : coinductive_llist @ a,X1 : a,X2 : a] : (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ X2 @ X0) @ (koenig916195507_paths @ a @ graph)) | (member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ X2 @ X0) @ ys) @ (koenig916195507_paths @ a @ graph))) & (graph @ X1 @ X2) & (x = ((coinductive_LCons @ a @ X1 @ (coinductive_LCons @ a @ X2 @ X0))))) | (x = coinductive_LNil @ a) | ? [X3 : a] : (x = ((coinductive_LCons @ a @ X3 @ coinductive_LNil @ a))))),
% 2.91/0.85 inference(rectify,[],[f271])).
% 2.91/0.85 thf(f386,plain,(
% 2.91/0.85 ~(? [X3 : a] : (x = ((coinductive_LCons @ a @ X3 @ coinductive_LNil @ a))) | ? [X1 : a,X0 : coinductive_llist @ a,X2 : a] : (($true = ((graph @ X1 @ X2))) & (($true = ((member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ X2 @ X0) @ ys) @ (koenig916195507_paths @ a @ graph)))) | (((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ X2 @ X0) @ (koenig916195507_paths @ a @ graph))) = $true)) & (x = ((coinductive_LCons @ a @ X1 @ (coinductive_LCons @ a @ X2 @ X0))))) | (x = coinductive_LNil @ a))),
% 2.91/0.85 inference(fool_elimination,[],[f385])).
% 2.91/0.85 thf(f640,plain,(
% 2.91/0.85 ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : ((coinductive_LNil @ X0 = ((coinductive_lappend @ X0 @ X1 @ X2))) <=> ((coinductive_LNil @ X0 = X1) & (coinductive_LNil @ X0 = X2)))),
% 2.91/0.85 inference(fool_elimination,[],[f16])).
% 2.91/0.85 thf(f663,plain,(
% 2.91/0.85 ! [X0 : $tType,X1 : X0,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0,X4 : X0] : ((((coinductive_LCons @ X0 @ X1 @ X2)) = ((coinductive_LCons @ X0 @ X4 @ X3))) = (X1 = X4) & (X2 = X3))),
% 2.91/0.85 inference(rectify,[],[f13])).
% 2.91/0.85 thf(f664,plain,(
% 2.91/0.85 ! [X0 : $tType,X4 : X0,X3 : coinductive_llist @ X0,X2 : coinductive_llist @ X0,X1 : X0] : (((X2 = X3) & (X1 = X4)) <=> (((coinductive_LCons @ X0 @ X1 @ X2)) = ((coinductive_LCons @ X0 @ X4 @ X3))))),
% 2.91/0.85 inference(fool_elimination,[],[f663])).
% 2.91/0.85 thf(f782,plain,(
% 2.91/0.85 ! [X0 : $tType,X2 : X0,X1 : coinductive_llist @ X0,X3 : coinductive_llist @ X0] : (((coinductive_LCons @ X0 @ X2 @ (coinductive_lappend @ X0 @ X3 @ X1))) = ((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ X2 @ X3) @ X1)))),
% 2.91/0.85 inference(rectify,[],[f11])).
% 2.91/0.85 thf(f913,plain,(
% 2.91/0.85 ! [X0 : $tType,X1 : coinductive_llist @ X0] : (? [X3 : coinductive_llist @ X0,X2 : X0] : (((coinductive_LCons @ X0 @ X2 @ X3)) = X1) | (coinductive_LNil @ X0 = X1))),
% 2.91/0.85 inference(ennf_transformation,[],[f18])).
% 2.91/0.85 thf(f943,plain,(
% 2.91/0.85 ! [X3 : a] : (x != ((coinductive_LCons @ a @ X3 @ coinductive_LNil @ a))) & (x != coinductive_LNil @ a) & ! [X2 : a,X0 : coinductive_llist @ a,X1 : a] : (((((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ X2 @ X0) @ (koenig916195507_paths @ a @ graph))) != $true) & ($true != ((member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ X2 @ X0) @ ys) @ (koenig916195507_paths @ a @ graph))))) | ($true != ((graph @ X1 @ X2))) | (x != ((coinductive_LCons @ a @ X1 @ (coinductive_LCons @ a @ X2 @ X0)))))),
% 2.91/0.85 inference(ennf_transformation,[],[f386])).
% 2.91/0.85 thf(f1062,plain,(
% 2.91/0.85 ! [X0 : $tType,X1 : coinductive_llist @ X0,X2 : X0] : (coinductive_LNil @ X0 != ((coinductive_LCons @ X0 @ X2 @ X1)))),
% 2.91/0.85 inference(rectify,[],[f17])).
% 2.91/0.85 thf(f1072,plain,(
% 2.91/0.85 ! [X0 : $tType,X1 : coinductive_llist @ X0] : (? [X2 : coinductive_llist @ X0,X3 : X0] : (((coinductive_LCons @ X0 @ X3 @ X2)) = X1) | (coinductive_LNil @ X0 = X1))),
% 2.91/0.85 inference(rectify,[],[f913])).
% 2.91/0.85 thf(f1073,plain,(
% 2.91/0.85 ! [X0 : $tType,X1 : coinductive_llist @ X0] : ((((coinductive_LCons @ X0 @ (sK23 @ X0 @ X1) @ (sK22 @ X0 @ X1))) = X1) | (coinductive_LNil @ X0 = X1))),
% 2.91/0.85 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X6,sK3 @ X0 @ X2 @ X1),skolemize(X6,sK3 @ X0 @ X2 @ X1)],[f1072])).
% 2.91/0.85 thf(f1084,plain,(
% 2.91/0.85 ! [X0 : $tType,X1 : X0,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0] : (((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ X1 @ X3) @ X2)) = ((coinductive_LCons @ X0 @ X1 @ (coinductive_lappend @ X0 @ X3 @ X2))))),
% 2.91/0.85 inference(rectify,[],[f782])).
% 2.91/0.85 thf(f1097,plain,(
% 2.91/0.85 ! [X0 : a] : (x != ((coinductive_LCons @ a @ X0 @ coinductive_LNil @ a))) & (x != coinductive_LNil @ a) & ! [X1 : a,X2 : coinductive_llist @ a,X3 : a] : (((((member @ coinductive_llist @ a @ (coinductive_LCons @ a @ X1 @ X2) @ (koenig916195507_paths @ a @ graph))) != $true) & (((member @ coinductive_llist @ a @ (coinductive_lappend @ a @ (coinductive_LCons @ a @ X1 @ X2) @ ys) @ (koenig916195507_paths @ a @ graph))) != $true)) | ($true != ((graph @ X3 @ X1))) | (x != ((coinductive_LCons @ a @ X3 @ (coinductive_LCons @ a @ X1 @ X2)))))),
% 2.91/0.85 inference(rectify,[],[f943])).
% 2.91/0.85 thf(f1213,plain,(
% 2.91/0.85 ! [X0 : $tType,X4 : X0,X3 : coinductive_llist @ X0,X2 : coinductive_llist @ X0,X1 : X0] : ((((X2 = X3) & (X1 = X4)) | (((coinductive_LCons @ X0 @ X1 @ X2)) != ((coinductive_LCons @ X0 @ X4 @ X3)))) & ((((coinductive_LCons @ X0 @ X1 @ X2)) = ((coinductive_LCons @ X0 @ X4 @ X3))) | ((X2 != X3) | (X1 != X4))))),
% 2.91/0.85 inference(nnf_transformation,[],[f664])).
% 2.91/0.85 thf(f1214,plain,(
% 2.91/0.85 ! [X0 : $tType,X4 : X0,X3 : coinductive_llist @ X0,X2 : coinductive_llist @ X0,X1 : X0] : ((((X2 = X3) & (X1 = X4)) | (((coinductive_LCons @ X0 @ X1 @ X2)) != ((coinductive_LCons @ X0 @ X4 @ X3)))) & ((((coinductive_LCons @ X0 @ X1 @ X2)) = ((coinductive_LCons @ X0 @ X4 @ X3))) | (X2 != X3) | (X1 != X4)))),
% 2.91/0.85 inference(flattening,[],[f1213])).
% 2.91/0.85 thf(f1215,plain,(
% 2.91/0.85 ! [X0 : $tType,X1 : X0,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0,X4 : X0] : ((((X2 = X3) & (X1 = X4)) | (((coinductive_LCons @ X0 @ X1 @ X2)) != ((coinductive_LCons @ X0 @ X4 @ X3)))) & ((((coinductive_LCons @ X0 @ X1 @ X2)) = ((coinductive_LCons @ X0 @ X4 @ X3))) | (X2 != X3) | (X1 != X4)))),
% 2.91/0.85 inference(rectify,[],[f1214])).
% 2.91/0.85 thf(f1257,plain,(
% 2.91/0.85 ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : (((coinductive_LNil @ X0 = ((coinductive_lappend @ X0 @ X1 @ X2))) | ((coinductive_LNil @ X0 != X1) | (coinductive_LNil @ X0 != X2))) & (((coinductive_LNil @ X0 = X1) & (coinductive_LNil @ X0 = X2)) | (coinductive_LNil @ X0 != ((coinductive_lappend @ X0 @ X1 @ X2)))))),
% 2.91/0.85 inference(nnf_transformation,[],[f640])).
% 2.91/0.85 thf(f1258,plain,(
% 2.91/0.85 ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : (((coinductive_LNil @ X0 = ((coinductive_lappend @ X0 @ X1 @ X2))) | (coinductive_LNil @ X0 != X1) | (coinductive_LNil @ X0 != X2)) & (((coinductive_LNil @ X0 = X1) & (coinductive_LNil @ X0 = X2)) | (coinductive_LNil @ X0 != ((coinductive_lappend @ X0 @ X1 @ X2)))))),
% 2.91/0.85 inference(flattening,[],[f1257])).
% 2.91/0.85 thf(f1259,plain,(
% 2.91/0.85 ! [X0 : $tType,X1 : coinductive_llist @ X0,X2 : coinductive_llist @ X0] : (((coinductive_LNil @ X0 = ((coinductive_lappend @ X0 @ X2 @ X1))) | (coinductive_LNil @ X0 != X2) | (coinductive_LNil @ X0 != X1)) & (((coinductive_LNil @ X0 = X2) & (coinductive_LNil @ X0 = X1)) | (coinductive_LNil @ X0 != ((coinductive_lappend @ X0 @ X2 @ X1)))))),
% 2.91/0.85 inference(rectify,[],[f1258])).
% 2.91/0.85 thf(f1307,plain,(
% 2.91/0.85 ( ! [X0 : $tType,X1 : coinductive_llist @ X0] : ((((coinductive_lappend @ X0 @ X1 @ coinductive_LNil @ X0)) = X1)) )),
% 2.91/0.85 inference(cnf_transformation,[],[f10])).
% 2.91/0.85 thf(f1345,plain,(
% 2.91/0.85 ( ! [X0 : $tType,X2 : X0,X1 : coinductive_llist @ X0] : ((coinductive_LNil @ X0 != ((coinductive_LCons @ X0 @ X2 @ X1)))) )),
% 2.91/0.85 inference(cnf_transformation,[],[f1062])).
% 2.91/0.85 thf(f1366,plain,(
% 2.91/0.85 ( ! [X0 : $tType,X1 : coinductive_llist @ X0] : ((coinductive_LNil @ X0 = X1) | (((coinductive_LCons @ X0 @ (sK23 @ X0 @ X1) @ (sK22 @ X0 @ X1))) = X1)) )),
% 2.91/0.85 inference(cnf_transformation,[],[f1073])).
% 2.91/0.85 thf(f1384,plain,(
% 2.91/0.85 (((coinductive_lappend @ a @ x @ ys)) = ((coinductive_LCons @ a @ xa @ coinductive_LNil @ a)))),
% 2.91/0.85 inference(cnf_transformation,[],[f268])).
% 2.91/0.85 thf(f1387,plain,(
% 2.91/0.85 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0,X1 : X0] : ((((coinductive_lappend @ X0 @ (coinductive_LCons @ X0 @ X1 @ X3) @ X2)) = ((coinductive_LCons @ X0 @ X1 @ (coinductive_lappend @ X0 @ X3 @ X2))))) )),
% 2.91/0.85 inference(cnf_transformation,[],[f1084])).
% 2.91/0.85 thf(f1477,plain,(
% 2.91/0.85 ( ! [X0 : a] : ((x != ((coinductive_LCons @ a @ X0 @ coinductive_LNil @ a)))) )),
% 2.91/0.85 inference(cnf_transformation,[],[f1097])).
% 2.91/0.85 thf(f1569,plain,(
% 2.91/0.85 (x = ((coinductive_LCons @ a @ x21 @ x22)))),
% 2.91/0.85 inference(cnf_transformation,[],[f269])).
% 2.91/0.85 thf(f1680,plain,(
% 2.91/0.85 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X3 : coinductive_llist @ X0,X1 : X0,X4 : X0] : ((((coinductive_LCons @ X0 @ X1 @ X2)) != ((coinductive_LCons @ X0 @ X4 @ X3))) | (X2 = X3)) )),
% 2.91/0.85 inference(cnf_transformation,[],[f1215])).
% 2.91/0.85 thf(f1750,plain,(
% 2.91/0.85 ( ! [X0 : $tType,X2 : coinductive_llist @ X0,X1 : coinductive_llist @ X0] : ((coinductive_LNil @ X0 != ((coinductive_lappend @ X0 @ X2 @ X1))) | (coinductive_LNil @ X0 = X2)) )),
% 2.91/0.85 inference(cnf_transformation,[],[f1259])).
% 2.91/0.85 thf(f1949,definition,(
% 2.91/0.85 spl106_2 <=> (x = ((coinductive_LCons @ a @ x21 @ x22)))),
% 2.91/0.85 introduced(definition,[new_symbols(definition,[spl106_2])],[avatar_definition])).
% 2.91/0.85 thf(f1951,plain,(
% 2.91/0.85 (x = ((coinductive_LCons @ a @ x21 @ x22))) | ~spl106_2),
% 2.91/0.85 inference(avatar_component_clause,[],[f1949])).
% 2.91/0.85 thf(f1952,plain,(
% 2.91/0.85 spl106_2),
% 2.91/0.85 inference(avatar_split_clause,[],[f1569,f1949])).
% 2.91/0.85 thf(f1974,definition,(
% 2.91/0.85 spl106_7 <=> (((coinductive_lappend @ a @ x @ ys)) = ((coinductive_LCons @ a @ xa @ coinductive_LNil @ a)))),
% 2.91/0.85 introduced(definition,[new_symbols(definition,[spl106_7])],[avatar_definition])).
% 2.91/0.85 thf(f1976,plain,(
% 2.91/0.85 (((coinductive_lappend @ a @ x @ ys)) = ((coinductive_LCons @ a @ xa @ coinductive_LNil @ a))) | ~spl106_7),
% 2.91/0.85 inference(avatar_component_clause,[],[f1974])).
% 2.91/0.85 thf(f1977,plain,(
% 2.91/0.85 spl106_7),
% 2.91/0.85 inference(avatar_split_clause,[],[f1384,f1974])).
% 2.91/0.85 thf(f1989,plain,(
% 2.91/0.85 ( ! [X0 : a] : ((((coinductive_LCons @ a @ x21 @ x22)) != ((coinductive_LCons @ a @ X0 @ coinductive_LNil @ a)))) ) | ~spl106_2),
% 2.91/0.85 inference(forward_demodulation,[],[f1477,f1951])).
% 2.91/0.85 thf(f1998,plain,(
% 2.91/0.85 (((coinductive_LCons @ a @ xa @ coinductive_LNil @ a)) = ((coinductive_lappend @ a @ (coinductive_LCons @ a @ x21 @ x22) @ ys))) | (~spl106_2 | ~spl106_7)),
% 2.91/0.85 inference(forward_demodulation,[],[f1976,f1951])).
% 2.91/0.85 thf(f2000,definition,(
% 2.91/0.85 spl106_10 <=> (((coinductive_LCons @ a @ xa @ coinductive_LNil @ a)) = ((coinductive_lappend @ a @ (coinductive_LCons @ a @ x21 @ x22) @ ys)))),
% 2.91/0.85 introduced(definition,[new_symbols(definition,[spl106_10])],[avatar_definition])).
% 2.91/0.85 thf(f2002,plain,(
% 2.91/0.85 (((coinductive_LCons @ a @ xa @ coinductive_LNil @ a)) = ((coinductive_lappend @ a @ (coinductive_LCons @ a @ x21 @ x22) @ ys))) | ~spl106_10),
% 2.91/0.85 inference(avatar_component_clause,[],[f2000])).
% 2.91/0.85 thf(f2003,plain,(
% 2.91/0.85 spl106_10 | ~spl106_2 | ~spl106_7),
% 2.91/0.85 inference(avatar_split_clause,[],[f1998,f1974,f1949,f2000])).
% 2.91/0.85 thf(f2011,plain,(
% 2.91/0.85 ( ! [X0 : coinductive_llist @ a,X1 : a] : ((((coinductive_LCons @ a @ x21 @ x22)) != ((coinductive_LCons @ a @ X1 @ X0))) | (((coinductive_LCons @ a @ (sK23 @ a @ X0) @ (sK22 @ a @ X0))) = X0)) ) | ~spl106_2),
% 2.91/0.85 inference(superposition,[],[f1989,f1366])).
% 2.91/0.85 thf(f2083,plain,(
% 2.91/0.85 (x22 = ((coinductive_LCons @ a @ (sK23 @ a @ x22) @ (sK22 @ a @ x22)))) | ~spl106_2),
% 2.91/0.85 inference(equality_resolution,[],[f2011])).
% 2.91/0.85 thf(f2085,definition,(
% 2.91/0.85 spl106_13 <=> (x22 = ((coinductive_LCons @ a @ (sK23 @ a @ x22) @ (sK22 @ a @ x22))))),
% 2.91/0.85 introduced(definition,[new_symbols(definition,[spl106_13])],[avatar_definition])).
% 2.91/0.85 thf(f2087,plain,(
% 2.91/0.85 (x22 = ((coinductive_LCons @ a @ (sK23 @ a @ x22) @ (sK22 @ a @ x22)))) | ~spl106_13),
% 2.91/0.85 inference(avatar_component_clause,[],[f2085])).
% 2.91/0.85 thf(f2088,plain,(
% 2.91/0.85 spl106_13 | ~spl106_2),
% 2.91/0.85 inference(avatar_split_clause,[],[f2083,f1949,f2085])).
% 2.91/0.85 thf(f2152,plain,(
% 2.91/0.85 (((coinductive_LCons @ a @ xa @ coinductive_LNil @ a)) = ((coinductive_LCons @ a @ x21 @ (coinductive_lappend @ a @ x22 @ ys)))) | ~spl106_10),
% 2.91/0.85 inference(backward_demodulation,[],[f2002,f1387])).
% 2.91/0.85 thf(f2153,plain,(
% 2.91/0.85 ( ! [X0 : coinductive_llist @ a] : ((((coinductive_lappend @ a @ x22 @ X0)) = ((coinductive_LCons @ a @ (sK23 @ a @ x22) @ (coinductive_lappend @ a @ (sK22 @ a @ x22) @ X0))))) ) | ~spl106_13),
% 2.91/0.85 inference(superposition,[],[f1387,f2087])).
% 2.91/0.85 thf(f2161,definition,(
% 2.91/0.85 spl106_22 <=> (((coinductive_LCons @ a @ xa @ coinductive_LNil @ a)) = ((coinductive_LCons @ a @ x21 @ (coinductive_lappend @ a @ x22 @ ys))))),
% 2.91/0.85 introduced(definition,[new_symbols(definition,[spl106_22])],[avatar_definition])).
% 2.91/0.85 thf(f2163,plain,(
% 2.91/0.85 (((coinductive_LCons @ a @ xa @ coinductive_LNil @ a)) = ((coinductive_LCons @ a @ x21 @ (coinductive_lappend @ a @ x22 @ ys)))) | ~spl106_22),
% 2.91/0.85 inference(avatar_component_clause,[],[f2161])).
% 2.91/0.85 thf(f2164,plain,(
% 2.91/0.85 spl106_22 | ~spl106_10),
% 2.91/0.85 inference(avatar_split_clause,[],[f2152,f2000,f2161])).
% 2.91/0.85 thf(f2169,plain,(
% 2.91/0.85 (coinductive_LNil @ a = ((coinductive_lappend @ a @ x22 @ ys))) | ~spl106_22),
% 2.91/0.85 inference(unit_resulting_resolution,[],[f1680,f2163])).
% 2.91/0.85 thf(f2190,definition,(
% 2.91/0.85 spl106_25 <=> (coinductive_LNil @ a = ((coinductive_lappend @ a @ x22 @ ys)))),
% 2.91/0.85 introduced(definition,[new_symbols(definition,[spl106_25])],[avatar_definition])).
% 2.91/0.85 thf(f2192,plain,(
% 2.91/0.85 (coinductive_LNil @ a = ((coinductive_lappend @ a @ x22 @ ys))) | ~spl106_25),
% 2.91/0.85 inference(avatar_component_clause,[],[f2190])).
% 2.91/0.85 thf(f2193,plain,(
% 2.91/0.85 spl106_25 | ~spl106_22),
% 2.91/0.85 inference(avatar_split_clause,[],[f2169,f2161,f2190])).
% 2.91/0.85 thf(f2420,plain,(
% 2.91/0.85 ( ! [X0 : coinductive_llist @ a] : ((coinductive_LNil @ a != ((coinductive_lappend @ a @ x22 @ X0)))) ) | ~spl106_13),
% 2.91/0.85 inference(superposition,[],[f1345,f2153])).
% 2.91/0.85 thf(f2630,plain,(
% 2.91/0.85 (coinductive_LNil @ a = x22) | (coinductive_LNil @ a != coinductive_LNil @ a) | ~spl106_25),
% 2.91/0.85 inference(superposition,[],[f1750,f2192])).
% 2.91/0.85 thf(f2632,plain,(
% 2.91/0.85 (coinductive_LNil @ a = x22) | ~spl106_25),
% 2.91/0.85 inference(trivial_inequality_removal,[],[f2630])).
% 2.91/0.85 thf(f2636,definition,(
% 2.91/0.85 spl106_60 <=> (coinductive_LNil @ a = x22)),
% 2.91/0.85 introduced(definition,[new_symbols(definition,[spl106_60])],[avatar_definition])).
% 2.91/0.85 thf(f2639,plain,(
% 2.91/0.85 spl106_60 | ~spl106_25),
% 2.91/0.85 inference(avatar_split_clause,[],[f2632,f2190,f2636])).
% 2.91/0.85 thf(f3223,plain,(
% 2.91/0.85 (coinductive_LNil @ a != x22) | ~spl106_13),
% 2.91/0.85 inference(superposition,[],[f2420,f1307])).
% 2.91/0.85 thf(f3235,plain,(
% 2.91/0.85 ~spl106_60 | ~spl106_13),
% 2.91/0.85 inference(avatar_split_clause,[],[f3223,f2085,f2636])).
% 2.91/0.85 cnf(s2, plain, spl106_2, inference(sat_conversion,[],[f1952])).
% 2.91/0.85 cnf(s7, plain, spl106_7, inference(sat_conversion,[],[f1977])).
% 2.91/0.85 cnf(s10, plain, ~spl106_2 | ~spl106_7 | spl106_10, inference(sat_conversion,[],[f2003])).
% 2.91/0.85 cnf(s21, plain, ~spl106_2 | spl106_13, inference(sat_conversion,[],[f2088])).
% 2.91/0.85 cnf(s29, plain, ~spl106_10 | spl106_22, inference(sat_conversion,[],[f2164])).
% 2.91/0.85 cnf(s31, plain, ~spl106_22 | spl106_25, inference(sat_conversion,[],[f2193])).
% 2.91/0.85 cnf(s90, plain, ~spl106_25 | spl106_60, inference(sat_conversion,[],[f2639])).
% 2.91/0.85 cnf(s142, plain, ~spl106_13 | ~spl106_60, inference(sat_conversion,[],[f3235])).
% 2.91/0.85 cnf(s144, plain, spl106_13, inference(rat,[],[s21,s2])).
% 2.91/0.85 cnf(s145, plain, spl106_10, inference(rat,[],[s10,s7,s2])).
% 2.91/0.85 cnf(s147, plain, ~spl106_60, inference(rat,[],[s142,s144])).
% 2.91/0.85 cnf(s148, plain, spl106_22, inference(rat,[],[s29,s145])).
% 2.91/0.85 cnf(s153, plain, ~spl106_25, inference(rat,[],[s90,s147])).
% 2.91/0.85 cnf(s156, plain, $false, inference(rat,[],[s31,s153,s148])).
% 2.91/0.85 thf(f3242,plain,(
% 2.91/0.85 $false),
% 2.91/0.85 inference(avatar_sat_refutation,[],[s156])).
% 2.91/0.85 % SZS output end Proof for theBenchmark
% 2.91/0.85 % (2988162)------------------------------
% 2.91/0.85 % (2988162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/0.85 % (2988162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/0.85 % (2988162)CaDiCaL version: 2.1.3
% 2.91/0.85 % (2988162)Termination reason: Refutation
% 2.91/0.85 % (2988162)Time elapsed: 0.195 s
% 2.91/0.85 % (2988162)Peak memory usage: 16 MB
% 2.91/0.85 % (2988162)Instructions burned: 326 (million)
% 2.91/0.85 % (2988074)Success in time 0.564 s
% 2.91/0.85 % Vampire exiting
%------------------------------------------------------------------------------