%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU974^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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 08:32:04 AM UTC 2026
% Result : Theorem 0.09s 0.22s
% Output : Refutation 0.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU974^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Tue Sep 29 14:54:18 UTC 2026
% 0.00/0.10 % CPUTime :
% 0.00/0.10 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.12 Running higher-order theorem proving
% 0.09/0.13 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.22 % (212769)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.09/0.22 % (212787)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.09/0.22 % (212787)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.09/0.22 % (212783)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=1318615555: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.09/0.22 % (212784)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3085599786:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.09/0.22 % (212782)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2287389872:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.09/0.22 % (212781)lrs+10_16_si=on:nwc=1.5:random_seed=2084165937:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.09/0.22 % (212780)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=224969119:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.09/0.22 % (212785)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3772752613:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.09/0.22 % (212787)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=3979531448:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.09/0.22 % (212782)Instruction limit reached!
% 0.09/0.22 % (212782)------------------------------
% 0.09/0.22 % (212782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212782)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212782)Termination reason: Instruction limit
% 0.09/0.22 % (212782)Termination phase: Property scanning
% 0.09/0.22 % (212782)Time elapsed: 0.001 s
% 0.09/0.22 % (212782)Peak memory usage: 10 MB
% 0.09/0.22 % (212782)Instructions burned: 3 (million)
% 0.09/0.22 % (212781)Instruction limit reached!
% 0.09/0.22 % (212781)------------------------------
% 0.09/0.22 % (212781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212781)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212781)Termination reason: Instruction limit
% 0.09/0.22 % (212781)Termination phase: Saturation
% 0.09/0.22 % (212781)Time elapsed: 0.005 s
% 0.09/0.22 % (212781)Peak memory usage: 12 MB
% 0.09/0.22 % (212781)Instructions burned: 18 (million)
% 0.09/0.22 % (212784)Instruction limit reached!
% 0.09/0.22 % (212784)------------------------------
% 0.09/0.22 % (212784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212784)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212784)Termination reason: Instruction limit
% 0.09/0.22 % (212784)Termination phase: Saturation
% 0.09/0.22 % (212784)Time elapsed: 0.007 s
% 0.09/0.22 % (212784)Peak memory usage: 12 MB
% 0.09/0.22 % (212784)Instructions burned: 24 (million)
% 0.09/0.22 % (212800)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=219538066:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.09/0.22 % (212800)Instruction limit reached!
% 0.09/0.22 % (212800)------------------------------
% 0.09/0.22 % (212800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212800)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212800)Termination reason: Instruction limit
% 0.09/0.22 % (212800)Termination phase: Saturation
% 0.09/0.22 % (212800)Time elapsed: 0.001 s
% 0.09/0.22 % (212800)Peak memory usage: 11 MB
% 0.09/0.22 % (212800)Instructions burned: 3 (million)
% 0.09/0.22 % (212805)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.09/0.22 % (212803)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=4155969679:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.09/0.22 % (212805)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1599940674:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.09/0.22 % (212803)Instruction limit reached!
% 0.09/0.22 % (212803)------------------------------
% 0.09/0.22 % (212803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212803)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212803)Termination reason: Instruction limit
% 0.09/0.22 % (212803)Termination phase: Saturation
% 0.09/0.22 % (212803)Time elapsed: 0.002 s
% 0.09/0.22 % (212803)Peak memory usage: 12 MB
% 0.09/0.22 % (212803)Instructions burned: 6 (million)
% 0.09/0.22 % (212805)Instruction limit reached!
% 0.09/0.22 % (212805)------------------------------
% 0.09/0.22 % (212805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212805)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212805)Termination reason: Instruction limit
% 0.09/0.22 % (212805)Termination phase: Saturation
% 0.09/0.22 % (212805)Time elapsed: 0.002 s
% 0.09/0.22 % (212805)Peak memory usage: 12 MB
% 0.09/0.22 % (212805)Instructions burned: 7 (million)
% 0.09/0.22 % (212785)Instruction limit reached!
% 0.09/0.22 % (212785)------------------------------
% 0.09/0.22 % (212785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212785)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212785)Termination reason: Instruction limit
% 0.09/0.22 % (212785)Termination phase: Saturation
% 0.09/0.22 % (212785)Time elapsed: 0.021 s
% 0.09/0.22 % (212785)Peak memory usage: 13 MB
% 0.09/0.22 % (212785)Instructions burned: 78 (million)
% 0.09/0.22 % (212780)Instruction limit reached!
% 0.09/0.22 % (212780)------------------------------
% 0.09/0.22 % (212780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212780)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212780)Termination reason: Instruction limit
% 0.09/0.22 % (212780)Termination phase: Saturation
% 0.09/0.22 % (212780)Time elapsed: 0.022 s
% 0.09/0.22 % (212780)Peak memory usage: 13 MB
% 0.09/0.22 % (212780)Instructions burned: 88 (million)
% 0.09/0.22 % (212810)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1326873002:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.09/0.22 % (212813)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.09/0.22 % (212813)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.09/0.22 % (212810)Instruction limit reached!
% 0.09/0.22 % (212810)------------------------------
% 0.09/0.22 % (212810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212810)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212810)Termination reason: Instruction limit
% 0.09/0.22 % (212810)Termination phase: Saturation
% 0.09/0.22 % (212810)Time elapsed: 0.004 s
% 0.09/0.22 % (212810)Peak memory usage: 12 MB
% 0.09/0.22 % (212810)Instructions burned: 13 (million)
% 0.09/0.22 % (212813)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=4188958047: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.09/0.22 % (212814)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=2794983799:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.09/0.22 % (212819)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.09/0.22 % (212816)lrs+10_1_si=on:cs=on:random_seed=2850149808:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.09/0.22 % (212819)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=2747813189:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.09/0.22 % (212819)Instruction limit reached!
% 0.09/0.22 % (212819)------------------------------
% 0.09/0.22 % (212819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212819)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212819)Termination reason: Instruction limit
% 0.09/0.22 % (212819)Termination phase: Saturation
% 0.09/0.22 % (212819)Time elapsed: 0.001 s
% 0.09/0.22 % (212819)Peak memory usage: 12 MB
% 0.09/0.22 % (212819)Instructions burned: 5 (million)
% 0.09/0.22 % (212816)Instruction limit reached!
% 0.09/0.22 % (212816)------------------------------
% 0.09/0.22 % (212816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212816)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212816)Termination reason: Instruction limit
% 0.09/0.22 % (212816)Termination phase: Saturation
% 0.09/0.22 % (212816)Time elapsed: 0.003 s
% 0.09/0.22 % (212816)Peak memory usage: 12 MB
% 0.09/0.22 % (212816)Instructions burned: 10 (million)
% 0.09/0.22 % (212813)Instruction limit reached!
% 0.09/0.22 % (212813)------------------------------
% 0.09/0.22 % (212813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212813)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212813)Termination reason: Instruction limit
% 0.09/0.22 % (212813)Termination phase: Saturation
% 0.09/0.22 % (212813)Time elapsed: 0.007 s
% 0.09/0.22 % (212813)Peak memory usage: 12 MB
% 0.09/0.22 % (212813)Instructions burned: 28 (million)
% 0.09/0.22 % (212821)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2845618060:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.09/0.22 % (212787)Instruction limit reached!
% 0.09/0.22 % (212787)------------------------------
% 0.09/0.22 % (212787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212787)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212787)Termination reason: Instruction limit
% 0.09/0.22 % (212787)Termination phase: Saturation
% 0.09/0.22 % (212787)Time elapsed: 0.043 s
% 0.09/0.22 % (212787)Peak memory usage: 13 MB
% 0.09/0.22 % (212787)Instructions burned: 159 (million)
% 0.09/0.22 % (212827)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=4012467198:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.09/0.22 % (212829)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3583135286:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.09/0.22 % (212830)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1285442063:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.09/0.22 % (212821)Instruction limit reached!
% 0.09/0.22 % (212821)------------------------------
% 0.09/0.22 % (212821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212821)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212821)Termination reason: Instruction limit
% 0.09/0.22 % (212821)Termination phase: Saturation
% 0.09/0.22 % (212821)Time elapsed: 0.012 s
% 0.09/0.22 % (212821)Peak memory usage: 12 MB
% 0.09/0.22 % (212821)Instructions burned: 40 (million)
% 0.09/0.22 % (212830)Instruction limit reached!
% 0.09/0.22 % (212830)------------------------------
% 0.09/0.22 % (212830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212830)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212830)Termination reason: Instruction limit
% 0.09/0.22 % (212830)Termination phase: Saturation
% 0.09/0.22 % (212830)Time elapsed: 0.005 s
% 0.09/0.22 % (212830)Peak memory usage: 12 MB
% 0.09/0.22 % (212830)Instructions burned: 16 (million)
% 0.09/0.22 % (212827) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-212769-212827"...
% 0.09/0.22 % (212829)Instruction limit reached!
% 0.09/0.22 % (212829)------------------------------
% 0.09/0.22 % (212829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212829)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212829)Termination reason: Instruction limit
% 0.09/0.22 % (212829)Termination phase: Saturation
% 0.09/0.22 % (212829)Time elapsed: 0.008 s
% 0.09/0.22 % (212829)Peak memory usage: 12 MB
% 0.09/0.22 % (212829)Instructions burned: 27 (million)
% 0.09/0.22 % (212814)Instruction limit reached!
% 0.09/0.22 % (212814)------------------------------
% 0.09/0.22 % (212814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212814)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212814)Termination reason: Instruction limit
% 0.09/0.22 % (212814)Termination phase: Saturation
% 0.09/0.22 % (212814)Time elapsed: 0.024 s
% 0.09/0.22 % (212814)Peak memory usage: 13 MB
% 0.09/0.22 % (212814)Instructions burned: 89 (million)
% 0.09/0.22 % (212833)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=686361389:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.09/0.22 % (212827)...printing done.
% 0.09/0.22 % (212840)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3474315432:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/14Mi)
% 0.09/0.22 % (212827)Refutation found. Thanks to Tanya!
% 0.09/0.22 % SZS status Theorem for theBenchmark
% 0.09/0.22 % SZS output start Proof for theBenchmark
% 0.09/0.22 thf(type_def_5, type, a: $tType).
% 0.09/0.22 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.09/0.22 thf(func_def_0, type, cR: (a > a)).
% 0.09/0.22 thf(func_def_1, type, cP: (a > a > a)).
% 0.09/0.22 thf(func_def_2, type, cL: (a > a)).
% 0.09/0.22 thf(func_def_3, type, cZ: a).
% 0.09/0.22 thf(func_def_7, type, sK0: ((a > $o) > a)).
% 0.09/0.22 thf(func_def_8, type, sK1: ((a > $o) > a)).
% 0.09/0.22 thf(func_def_9, type, sK2: a).
% 0.09/0.22 thf(func_def_10, type, sK3: a).
% 0.09/0.22 thf(func_def_11, type, sK4: ((a > $o) > a)).
% 0.09/0.22 thf(func_def_12, type, sK5: ((a > $o) > a)).
% 0.09/0.22 thf(func_def_13, type, sK6: (a > $o)).
% 0.09/0.22 thf(func_def_14, type, vNOT: ($o > $o)).
% 0.09/0.22 thf(func_def_15, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.09/0.22 thf(func_def_16, type, db0: !>[X0: $tType]:(X0)).
% 0.09/0.22 thf(func_def_17, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.09/0.22 thf(f1,conjecture,(
% 0.09/0.22 (! [X3 : (a > $o)] : (! [X2 : a,X4 : a] : ((X3 @ (cP @ X2 @ X4)) => ((X3 @ (cP @ (cL @ X2) @ (cL @ X4))) & ((X2 = cZ) <=> (X4 = cZ)) & (X3 @ (cP @ (cR @ X2) @ (cR @ X4))))) => ! [X4 : a,X2 : a] : ((X3 @ (cP @ X2 @ X4)) => (X2 = X4))) & ! [X1 : a,X0 : a] : (((cL @ (cP @ X0 @ X1))) = X0) & (((cL @ cZ)) = cZ) & ! [X1 : a,X0 : a] : (((cR @ (cP @ X0 @ X1))) = X1) & ! [X2 : a] : ((X2 = ((cP @ (cL @ X2) @ (cR @ X2)))) <=> (X2 != cZ)) & (((cR @ cZ)) = cZ)) => ! [X0 : a,X1 : a] : (? [X3 : (a > $o)] : ((X3 @ (cP @ X0 @ X1)) & ! [X2 : a,X4 : a] : ((X3 @ (cP @ X2 @ X4)) => (((X4 = cZ) => (X2 = cZ)) & (X3 @ (cP @ (cR @ X2) @ (cR @ X4))) & (X3 @ (cP @ (cL @ X2) @ (cL @ X4)))))) => ? [X3 : (a > $o)] : (! [X4 : a,X2 : a] : ((X3 @ (cP @ X2 @ X4)) => (((X4 = cZ) => (X2 = cZ)) & (X3 @ (cP @ (cL @ X2) @ (cL @ X4))) & (X3 @ (cP @ (cR @ X2) @ (cR @ X4))))) & (X3 @ (cP @ (cR @ X0) @ (cR @ X1)))))),
% 0.09/0.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cPU_LEM2C_pme)).
% 0.09/0.22 thf(f2,negated_conjecture,(
% 0.09/0.22 ~((! [X3 : (a > $o)] : (! [X2 : a,X4 : a] : ((X3 @ (cP @ X2 @ X4)) => ((X3 @ (cP @ (cL @ X2) @ (cL @ X4))) & ((X2 = cZ) <=> (X4 = cZ)) & (X3 @ (cP @ (cR @ X2) @ (cR @ X4))))) => ! [X4 : a,X2 : a] : ((X3 @ (cP @ X2 @ X4)) => (X2 = X4))) & ! [X1 : a,X0 : a] : (((cL @ (cP @ X0 @ X1))) = X0) & (((cL @ cZ)) = cZ) & ! [X1 : a,X0 : a] : (((cR @ (cP @ X0 @ X1))) = X1) & ! [X2 : a] : ((X2 = ((cP @ (cL @ X2) @ (cR @ X2)))) <=> (X2 != cZ)) & (((cR @ cZ)) = cZ)) => ! [X0 : a,X1 : a] : (? [X3 : (a > $o)] : ((X3 @ (cP @ X0 @ X1)) & ! [X2 : a,X4 : a] : ((X3 @ (cP @ X2 @ X4)) => (((X4 = cZ) => (X2 = cZ)) & (X3 @ (cP @ (cR @ X2) @ (cR @ X4))) & (X3 @ (cP @ (cL @ X2) @ (cL @ X4)))))) => ? [X3 : (a > $o)] : (! [X4 : a,X2 : a] : ((X3 @ (cP @ X2 @ X4)) => (((X4 = cZ) => (X2 = cZ)) & (X3 @ (cP @ (cL @ X2) @ (cL @ X4))) & (X3 @ (cP @ (cR @ X2) @ (cR @ X4))))) & (X3 @ (cP @ (cR @ X0) @ (cR @ X1))))))),
% 0.09/0.22 inference(negated_conjecture,[status(cth)],[f1])).
% 0.09/0.22 thf(f3,plain,(
% 0.09/0.22 ~((! [X0 : (a > $o)] : (! [X1 : a,X2 : a] : ((X0 @ (cP @ X1 @ X2)) => ((X0 @ (cP @ (cL @ X1) @ (cL @ X2))) & ((cZ = X1) <=> (cZ = X2)) & (X0 @ (cP @ (cR @ X1) @ (cR @ X2))))) => ! [X3 : a,X4 : a] : ((X0 @ (cP @ X4 @ X3)) => (X3 = X4))) & ! [X5 : a,X6 : a] : (((cL @ (cP @ X6 @ X5))) = X6) & (((cL @ cZ)) = cZ) & ! [X7 : a,X8 : a] : (((cR @ (cP @ X8 @ X7))) = X7) & ! [X9 : a] : ((((cP @ (cL @ X9) @ (cR @ X9))) = X9) <=> (cZ != X9)) & (((cR @ cZ)) = cZ)) => ! [X10 : a,X11 : a] : (? [X12 : (a > $o)] : ((X12 @ (cP @ X10 @ X11)) & ! [X13 : a,X14 : a] : ((X12 @ (cP @ X13 @ X14)) => (((cZ = X14) => (cZ = X13)) & (X12 @ (cP @ (cR @ X13) @ (cR @ X14))) & (X12 @ (cP @ (cL @ X13) @ (cL @ X14)))))) => ? [X15 : (a > $o)] : (! [X16 : a,X17 : a] : ((X15 @ (cP @ X17 @ X16)) => (((cZ = X16) => (cZ = X17)) & (X15 @ (cP @ (cL @ X17) @ (cL @ X16))) & (X15 @ (cP @ (cR @ X17) @ (cR @ X16))))) & (X15 @ (cP @ (cR @ X10) @ (cR @ X11))))))),
% 0.09/0.22 inference(rectify,[],[f2])).
% 0.09/0.22 thf(f4,plain,(
% 0.09/0.22 ~(((cZ = ((cR @ cZ))) & (cZ = ((cL @ cZ))) & ! [X7 : a,X8 : a] : (((cR @ (cP @ X8 @ X7))) = X7) & ! [X9 : a] : ((cZ != X9) <=> (((cP @ (cL @ X9) @ (cR @ X9))) = X9)) & ! [X0 : (a > $o)] : (! [X1 : a,X2 : a] : ((((X0 @ (cP @ X1 @ X2))) = $true) => (($true = ((X0 @ (cP @ (cR @ X1) @ (cR @ X2))))) & ((cZ = X1) <=> (cZ = X2)) & ($true = ((X0 @ (cP @ (cL @ X1) @ (cL @ X2))))))) => ! [X4 : a,X3 : a] : (($true = ((X0 @ (cP @ X4 @ X3)))) => (X3 = X4))) & ! [X6 : a,X5 : a] : (((cL @ (cP @ X6 @ X5))) = X6)) => ! [X11 : a,X10 : a] : (? [X12 : (a > $o)] : (! [X13 : a,X14 : a] : (($true = ((X12 @ (cP @ X13 @ X14)))) => ((((X12 @ (cP @ (cL @ X13) @ (cL @ X14)))) = $true) & ($true = ((X12 @ (cP @ (cR @ X13) @ (cR @ X14))))) & ((cZ = X14) => (cZ = X13)))) & ($true = ((X12 @ (cP @ X10 @ X11))))) => ? [X15 : (a > $o)] : (! [X16 : a,X17 : a] : (($true = ((X15 @ (cP @ X17 @ X16)))) => (($true = ((X15 @ (cP @ (cR @ X17) @ (cR @ X16))))) & (((X15 @ (cP @ (cL @ X17) @ (cL @ X16)))) = $true) & ((cZ = X16) => (cZ = X17)))) & ($true = ((X15 @ (cP @ (cR @ X10) @ (cR @ X11))))))))),
% 0.09/0.22 inference(fool_elimination,[],[f3])).
% 0.09/0.22 thf(f5,plain,(
% 0.09/0.22 ? [X11 : a,X10 : a] : (! [X15 : (a > $o)] : (($true != ((X15 @ (cP @ (cR @ X10) @ (cR @ X11))))) | ? [X16 : a,X17 : a] : ((((cZ != X17) & (cZ = X16)) | ($true != ((X15 @ (cP @ (cR @ X17) @ (cR @ X16))))) | (((X15 @ (cP @ (cL @ X17) @ (cL @ X16)))) != $true)) & ($true = ((X15 @ (cP @ X17 @ X16)))))) & ? [X12 : (a > $o)] : (($true = ((X12 @ (cP @ X10 @ X11)))) & ! [X13 : a,X14 : a] : (((((X12 @ (cP @ (cL @ X13) @ (cL @ X14)))) = $true) & ($true = ((X12 @ (cP @ (cR @ X13) @ (cR @ X14))))) & ((cZ = X13) | (cZ != X14))) | ($true != ((X12 @ (cP @ X13 @ X14))))))) & ((cZ = ((cR @ cZ))) & (cZ = ((cL @ cZ))) & ! [X7 : a,X8 : a] : (((cR @ (cP @ X8 @ X7))) = X7) & ! [X9 : a] : ((cZ != X9) <=> (((cP @ (cL @ X9) @ (cR @ X9))) = X9)) & ! [X0 : (a > $o)] : (? [X1 : a,X2 : a] : ((((X0 @ (cP @ X1 @ X2))) = $true) & (($true != ((X0 @ (cP @ (cR @ X1) @ (cR @ X2))))) | ($true != ((X0 @ (cP @ (cL @ X1) @ (cL @ X2))))) | ((cZ = X1) <~> (cZ = X2)))) | ! [X4 : a,X3 : a] : ((X3 = X4) | ($true != ((X0 @ (cP @ X4 @ X3)))))) & ! [X6 : a,X5 : a] : (((cL @ (cP @ X6 @ X5))) = X6))),
% 0.09/0.22 inference(ennf_transformation,[],[f4])).
% 0.09/0.22 thf(f6,plain,(
% 0.09/0.22 (cZ = ((cL @ cZ))) & ! [X0 : (a > $o)] : (? [X1 : a,X2 : a] : ((((X0 @ (cP @ X1 @ X2))) = $true) & (($true != ((X0 @ (cP @ (cR @ X1) @ (cR @ X2))))) | ($true != ((X0 @ (cP @ (cL @ X1) @ (cL @ X2))))) | ((cZ = X1) <~> (cZ = X2)))) | ! [X4 : a,X3 : a] : ((X3 = X4) | ($true != ((X0 @ (cP @ X4 @ X3)))))) & ! [X9 : a] : ((cZ != X9) <=> (((cP @ (cL @ X9) @ (cR @ X9))) = X9)) & (cZ = ((cR @ cZ))) & ? [X11 : a,X10 : a] : (! [X15 : (a > $o)] : (($true != ((X15 @ (cP @ (cR @ X10) @ (cR @ X11))))) | ? [X16 : a,X17 : a] : ((((cZ != X17) & (cZ = X16)) | ($true != ((X15 @ (cP @ (cR @ X17) @ (cR @ X16))))) | (((X15 @ (cP @ (cL @ X17) @ (cL @ X16)))) != $true)) & ($true = ((X15 @ (cP @ X17 @ X16)))))) & ? [X12 : (a > $o)] : (($true = ((X12 @ (cP @ X10 @ X11)))) & ! [X13 : a,X14 : a] : (((((X12 @ (cP @ (cL @ X13) @ (cL @ X14)))) = $true) & ($true = ((X12 @ (cP @ (cR @ X13) @ (cR @ X14))))) & ((cZ = X13) | (cZ != X14))) | ($true != ((X12 @ (cP @ X13 @ X14))))))) & ! [X6 : a,X5 : a] : (((cL @ (cP @ X6 @ X5))) = X6) & ! [X7 : a,X8 : a] : (((cR @ (cP @ X8 @ X7))) = X7)),
% 0.09/0.22 inference(flattening,[],[f5])).
% 0.09/0.22 thf(f7,plain,(
% 0.09/0.22 (cZ = ((cL @ cZ))) & ! [X0 : (a > $o)] : (? [X1 : a,X2 : a] : ((((X0 @ (cP @ X1 @ X2))) = $true) & (($true != ((X0 @ (cP @ (cR @ X1) @ (cR @ X2))))) | ($true != ((X0 @ (cP @ (cL @ X1) @ (cL @ X2))))) | (((cZ != X2) | (cZ != X1)) & ((cZ = X2) | (cZ = X1))))) | ! [X4 : a,X3 : a] : ((X3 = X4) | ($true != ((X0 @ (cP @ X4 @ X3)))))) & ! [X9 : a] : (((cZ != X9) | (((cP @ (cL @ X9) @ (cR @ X9))) != X9)) & ((((cP @ (cL @ X9) @ (cR @ X9))) = X9) | (cZ = X9))) & (cZ = ((cR @ cZ))) & ? [X11 : a,X10 : a] : (! [X15 : (a > $o)] : (($true != ((X15 @ (cP @ (cR @ X10) @ (cR @ X11))))) | ? [X16 : a,X17 : a] : ((((cZ != X17) & (cZ = X16)) | ($true != ((X15 @ (cP @ (cR @ X17) @ (cR @ X16))))) | (((X15 @ (cP @ (cL @ X17) @ (cL @ X16)))) != $true)) & ($true = ((X15 @ (cP @ X17 @ X16)))))) & ? [X12 : (a > $o)] : (($true = ((X12 @ (cP @ X10 @ X11)))) & ! [X13 : a,X14 : a] : (((((X12 @ (cP @ (cL @ X13) @ (cL @ X14)))) = $true) & ($true = ((X12 @ (cP @ (cR @ X13) @ (cR @ X14))))) & ((cZ = X13) | (cZ != X14))) | ($true != ((X12 @ (cP @ X13 @ X14))))))) & ! [X6 : a,X5 : a] : (((cL @ (cP @ X6 @ X5))) = X6) & ! [X7 : a,X8 : a] : (((cR @ (cP @ X8 @ X7))) = X7)),
% 0.09/0.22 inference(nnf_transformation,[],[f6])).
% 0.09/0.22 thf(f8,plain,(
% 0.09/0.22 (cZ = ((cL @ cZ))) & ! [X0 : (a > $o)] : (? [X1 : a,X2 : a] : ((((X0 @ (cP @ X1 @ X2))) = $true) & (($true != ((X0 @ (cP @ (cR @ X1) @ (cR @ X2))))) | ($true != ((X0 @ (cP @ (cL @ X1) @ (cL @ X2))))) | (((cZ != X2) | (cZ != X1)) & ((cZ = X2) | (cZ = X1))))) | ! [X3 : a,X4 : a] : ((X3 = X4) | ($true != ((X0 @ (cP @ X3 @ X4)))))) & ! [X5 : a] : (((cZ != X5) | (((cP @ (cL @ X5) @ (cR @ X5))) != X5)) & ((((cP @ (cL @ X5) @ (cR @ X5))) = X5) | (cZ = X5))) & (cZ = ((cR @ cZ))) & ? [X6 : a,X7 : a] : (! [X8 : (a > $o)] : (($true != ((X8 @ (cP @ (cR @ X7) @ (cR @ X6))))) | ? [X9 : a,X10 : a] : ((((cZ != X10) & (cZ = X9)) | ($true != ((X8 @ (cP @ (cR @ X10) @ (cR @ X9))))) | (((X8 @ (cP @ (cL @ X10) @ (cL @ X9)))) != $true)) & ($true = ((X8 @ (cP @ X10 @ X9)))))) & ? [X11 : (a > $o)] : ((((X11 @ (cP @ X7 @ X6))) = $true) & ! [X12 : a,X13 : a] : (((((X11 @ (cP @ (cL @ X12) @ (cL @ X13)))) = $true) & ($true = ((X11 @ (cP @ (cR @ X12) @ (cR @ X13))))) & ((cZ = X12) | (cZ != X13))) | ($true != ((X11 @ (cP @ X12 @ X13))))))) & ! [X14 : a,X15 : a] : (((cL @ (cP @ X14 @ X15))) = X14) & ! [X16 : a,X17 : a] : (((cR @ (cP @ X17 @ X16))) = X16)),
% 0.09/0.22 inference(rectify,[],[f7])).
% 0.09/0.22 thf(f9,plain,(
% 0.09/0.22 (cZ = ((cL @ cZ))) & ! [X0 : (a > $o)] : ((($true = ((X0 @ (cP @ (sK0 @ X0) @ (sK1 @ X0))))) & (($true != ((X0 @ (cP @ (cR @ (sK0 @ X0)) @ (cR @ (sK1 @ X0)))))) | ($true != ((X0 @ (cP @ (cL @ (sK0 @ X0)) @ (cL @ (sK1 @ X0)))))) | (((cZ != ((sK1 @ X0))) | (cZ != ((sK0 @ X0)))) & ((cZ = ((sK1 @ X0))) | (cZ = ((sK0 @ X0))))))) | ! [X3 : a,X4 : a] : ((X3 = X4) | ($true != ((X0 @ (cP @ X3 @ X4)))))) & ! [X5 : a] : (((cZ != X5) | (((cP @ (cL @ X5) @ (cR @ X5))) != X5)) & ((((cP @ (cL @ X5) @ (cR @ X5))) = X5) | (cZ = X5))) & (cZ = ((cR @ cZ))) & (! [X8 : (a > $o)] : (($true != ((X8 @ (cP @ (cR @ sK3) @ (cR @ sK2))))) | ((((cZ != ((sK5 @ X8))) & (cZ = ((sK4 @ X8)))) | ($true != ((X8 @ (cP @ (cR @ (sK5 @ X8)) @ (cR @ (sK4 @ X8)))))) | ($true != ((X8 @ (cP @ (cL @ (sK5 @ X8)) @ (cL @ (sK4 @ X8))))))) & ($true = ((X8 @ (cP @ (sK5 @ X8) @ (sK4 @ X8))))))) & (($true = ((sK6 @ (cP @ sK3 @ sK2)))) & ! [X12 : a,X13 : a] : ((($true = ((sK6 @ (cP @ (cL @ X12) @ (cL @ X13))))) & ($true = ((sK6 @ (cP @ (cR @ X12) @ (cR @ X13))))) & ((cZ = X12) | (cZ != X13))) | ($true != ((sK6 @ (cP @ X12 @ X13))))))) & ! [X14 : a,X15 : a] : (((cL @ (cP @ X14 @ X15))) = X14) & ! [X16 : a,X17 : a] : (((cR @ (cP @ X17 @ X16))) = X16)),
% 0.09/0.22 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,sK2,sK3,vAPP,vAPP,sK6]),skolemize(X10,sK5 @ X8),skolemize(X10,sK5 @ X8),skolemize(X6,sK2),skolemize(X7,sK3),skolemize(X10,sK5 @ X8),skolemize(X10,sK5 @ X8),skolemize(X11,sK6)],[f8])).
% 0.09/0.22 thf(f12,plain,(
% 0.09/0.22 ( ! [X12 : a,X13 : a] : ((cZ = X12) | (cZ != X13) | ($true != ((sK6 @ (cP @ X12 @ X13))))) )),
% 0.09/0.22 inference(cnf_transformation,[],[f9])).
% 0.09/0.22 thf(f13,plain,(
% 0.09/0.22 ( ! [X12 : a,X13 : a] : (($true = ((sK6 @ (cP @ (cR @ X12) @ (cR @ X13))))) | ($true != ((sK6 @ (cP @ X12 @ X13))))) )),
% 0.09/0.22 inference(cnf_transformation,[],[f9])).
% 0.09/0.22 thf(f14,plain,(
% 0.09/0.22 ( ! [X12 : a,X13 : a] : (($true = ((sK6 @ (cP @ (cL @ X12) @ (cL @ X13))))) | ($true != ((sK6 @ (cP @ X12 @ X13))))) )),
% 0.09/0.22 inference(cnf_transformation,[],[f9])).
% 0.09/0.22 thf(f15,plain,(
% 0.09/0.22 ($true = ((sK6 @ (cP @ sK3 @ sK2))))),
% 0.09/0.22 inference(cnf_transformation,[],[f9])).
% 0.09/0.22 thf(f16,plain,(
% 0.09/0.22 ( ! [X8 : (a > $o)] : (($true = ((X8 @ (cP @ (sK5 @ X8) @ (sK4 @ X8))))) | ($true != ((X8 @ (cP @ (cR @ sK3) @ (cR @ sK2)))))) )),
% 0.09/0.22 inference(cnf_transformation,[],[f9])).
% 0.09/0.22 thf(f17,plain,(
% 0.09/0.22 ( ! [X8 : (a > $o)] : (($true != ((X8 @ (cP @ (cL @ (sK5 @ X8)) @ (cL @ (sK4 @ X8)))))) | ($true != ((X8 @ (cP @ (cR @ sK3) @ (cR @ sK2))))) | (cZ = ((sK4 @ X8))) | ($true != ((X8 @ (cP @ (cR @ (sK5 @ X8)) @ (cR @ (sK4 @ X8))))))) )),
% 0.09/0.22 inference(cnf_transformation,[],[f9])).
% 0.09/0.22 thf(f18,plain,(
% 0.09/0.22 ( ! [X8 : (a > $o)] : (($true != ((X8 @ (cP @ (cL @ (sK5 @ X8)) @ (cL @ (sK4 @ X8)))))) | (cZ != ((sK5 @ X8))) | ($true != ((X8 @ (cP @ (cR @ sK3) @ (cR @ sK2))))) | ($true != ((X8 @ (cP @ (cR @ (sK5 @ X8)) @ (cR @ (sK4 @ X8))))))) )),
% 0.09/0.22 inference(cnf_transformation,[],[f9])).
% 0.09/0.22 thf(f27,definition,(
% 0.09/0.22 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.09/0.22 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.09/0.22 thf(f29,plain,(
% 0.09/0.22 ( ! [X12 : a] : (($true != ((sK6 @ (cP @ X12 @ cZ)))) | (cZ = X12)) )),
% 0.09/0.22 inference(equality_resolution,[],[f12])).
% 0.09/0.22 thf(f30,plain,(
% 0.09/0.22 ( ! [X0 : a] : (($true != $true) | (cZ = X0) | ($false = ((sK6 @ (cP @ X0 @ cZ))))) )),
% 0.09/0.22 inference(superposition,[],[f29,f27])).
% 0.09/0.22 thf(f31,plain,(
% 0.09/0.22 ( ! [X0 : a] : (($false = ((sK6 @ (cP @ X0 @ cZ)))) | (cZ = X0)) )),
% 0.09/0.22 inference(trivial_inequality_removal,[],[f30])).
% 0.09/0.22 thf(f94,plain,(
% 0.09/0.22 ($true != $true) | ($true != ((sK6 @ (cP @ (sK5 @ sK6) @ (sK4 @ sK6))))) | (((sK6 @ (cP @ (cR @ sK3) @ (cR @ sK2)))) != $true) | ($true != ((sK6 @ (cP @ (cR @ (sK5 @ sK6)) @ (cR @ (sK4 @ sK6)))))) | (cZ = ((sK4 @ sK6)))),
% 0.09/0.22 inference(superposition,[],[f17,f14])).
% 0.09/0.22 thf(f99,plain,(
% 0.09/0.22 (((sK6 @ (cP @ (cR @ sK3) @ (cR @ sK2)))) != $true) | (cZ = ((sK4 @ sK6))) | ($true != ((sK6 @ (cP @ (cR @ (sK5 @ sK6)) @ (cR @ (sK4 @ sK6)))))) | ($true != ((sK6 @ (cP @ (sK5 @ sK6) @ (sK4 @ sK6)))))),
% 0.09/0.22 inference(trivial_inequality_removal,[],[f94])).
% 0.09/0.22 thf(f110,plain,(
% 0.09/0.22 (((sK6 @ (cP @ (cR @ sK3) @ (cR @ sK2)))) != $true) | (cZ = ((sK4 @ sK6))) | ($true != ((sK6 @ (cP @ (cR @ (sK5 @ sK6)) @ (cR @ (sK4 @ sK6))))))),
% 0.09/0.22 inference(forward_subsumption_resolution,[],[f99,f16])).
% 0.09/0.22 thf(f112,definition,(
% 0.09/0.22 spl7_1 <=> (cZ = ((sK4 @ sK6)))),
% 0.09/0.22 introduced(definition,[new_symbols(definition,[spl7_1])],[avatar_definition])).
% 0.09/0.22 thf(f114,plain,(
% 0.09/0.22 (cZ = ((sK4 @ sK6))) | ~spl7_1),
% 0.09/0.22 inference(avatar_component_clause,[],[f112])).
% 0.09/0.22 thf(f116,definition,(
% 0.09/0.22 spl7_2 <=> (((sK6 @ (cP @ (cR @ sK3) @ (cR @ sK2)))) = $true)),
% 0.09/0.22 introduced(definition,[new_symbols(definition,[spl7_2])],[avatar_definition])).
% 0.09/0.22 thf(f117,plain,(
% 0.09/0.22 (((sK6 @ (cP @ (cR @ sK3) @ (cR @ sK2)))) = $true) | ~spl7_2),
% 0.09/0.22 inference(avatar_component_clause,[],[f116])).
% 0.09/0.22 thf(f118,plain,(
% 0.09/0.22 (((sK6 @ (cP @ (cR @ sK3) @ (cR @ sK2)))) != $true) | spl7_2),
% 0.09/0.22 inference(avatar_component_clause,[],[f116])).
% 0.09/0.22 thf(f120,definition,(
% 0.09/0.22 spl7_3 <=> ($true = ((sK6 @ (cP @ (cR @ (sK5 @ sK6)) @ (cR @ (sK4 @ sK6))))))),
% 0.09/0.22 introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition])).
% 0.09/0.22 thf(f121,plain,(
% 0.09/0.22 ($true = ((sK6 @ (cP @ (cR @ (sK5 @ sK6)) @ (cR @ (sK4 @ sK6)))))) | ~spl7_3),
% 0.09/0.22 inference(avatar_component_clause,[],[f120])).
% 0.09/0.22 thf(f122,plain,(
% 0.09/0.22 ($true != ((sK6 @ (cP @ (cR @ (sK5 @ sK6)) @ (cR @ (sK4 @ sK6)))))) | spl7_3),
% 0.09/0.22 inference(avatar_component_clause,[],[f120])).
% 0.09/0.22 thf(f123,plain,(
% 0.09/0.22 spl7_1 | ~spl7_2 | ~spl7_3),
% 0.09/0.22 inference(avatar_split_clause,[],[f110,f120,f116,f112])).
% 0.09/0.22 thf(f131,plain,(
% 0.09/0.22 (((sK6 @ (cP @ (cR @ sK3) @ (cR @ sK2)))) != $true) | ($true != ((sK6 @ (cP @ (sK5 @ sK6) @ (sK4 @ sK6))))) | ($true != ((sK6 @ (cP @ (cR @ (sK5 @ sK6)) @ (cR @ (sK4 @ sK6)))))) | (cZ != ((sK5 @ sK6))) | ($true != $true)),
% 0.09/0.22 inference(superposition,[],[f18,f14])).
% 0.09/0.22 thf(f146,plain,(
% 0.09/0.22 (cZ != ((sK5 @ sK6))) | ($true != ((sK6 @ (cP @ (sK5 @ sK6) @ (sK4 @ sK6))))) | (((sK6 @ (cP @ (cR @ sK3) @ (cR @ sK2)))) != $true) | ($true != ((sK6 @ (cP @ (cR @ (sK5 @ sK6)) @ (cR @ (sK4 @ sK6))))))),
% 0.09/0.22 inference(trivial_inequality_removal,[],[f131])).
% 0.09/0.22 thf(f435,plain,(
% 0.09/0.22 ($true != $true) | ($true != ((sK6 @ (cP @ sK3 @ sK2)))) | spl7_2),
% 0.09/0.22 inference(superposition,[],[f118,f13])).
% 0.09/0.22 thf(f437,plain,(
% 0.09/0.22 ($true != ((sK6 @ (cP @ sK3 @ sK2)))) | spl7_2),
% 0.09/0.22 inference(trivial_inequality_removal,[],[f435])).
% 0.09/0.22 thf(f439,plain,(
% 0.09/0.22 $false | spl7_2),
% 0.09/0.22 inference(forward_subsumption_resolution,[],[f437,f15])).
% 0.09/0.22 thf(f440,plain,(
% 0.09/0.22 spl7_2),
% 0.09/0.22 inference(avatar_contradiction_clause,[],[f439])).
% 0.09/0.22 thf(f441,plain,(
% 0.09/0.22 (cZ != ((sK5 @ sK6))) | ($true != ((sK6 @ (cP @ (cR @ (sK5 @ sK6)) @ (cR @ (sK4 @ sK6)))))) | (((sK6 @ (cP @ (cR @ sK3) @ (cR @ sK2)))) != $true)),
% 0.09/0.22 inference(forward_subsumption_resolution,[],[f146,f16])).
% 0.09/0.22 thf(f448,plain,(
% 0.09/0.22 ($true != $true) | ($true != ((sK6 @ (cP @ (sK5 @ sK6) @ (sK4 @ sK6))))) | spl7_3),
% 0.09/0.22 inference(superposition,[],[f122,f13])).
% 0.09/0.22 thf(f451,plain,(
% 0.09/0.22 ($true != ((sK6 @ (cP @ (sK5 @ sK6) @ (sK4 @ sK6))))) | spl7_3),
% 0.09/0.22 inference(trivial_inequality_removal,[],[f448])).
% 0.09/0.22 thf(f466,plain,(
% 0.09/0.22 ($true != $true) | (((sK6 @ (cP @ (cR @ sK3) @ (cR @ sK2)))) != $true) | spl7_3),
% 0.09/0.22 inference(superposition,[],[f451,f16])).
% 0.09/0.22 thf(f468,plain,(
% 0.09/0.22 (((sK6 @ (cP @ (cR @ sK3) @ (cR @ sK2)))) != $true) | spl7_3),
% 0.09/0.22 inference(trivial_inequality_removal,[],[f466])).
% 0.09/0.22 thf(f470,plain,(
% 0.09/0.22 $false | (~spl7_2 | spl7_3)),
% 0.09/0.22 inference(forward_subsumption_resolution,[],[f468,f117])).
% 0.09/0.22 thf(f471,plain,(
% 0.09/0.22 ~spl7_2 | spl7_3),
% 0.09/0.22 inference(avatar_contradiction_clause,[],[f470])).
% 0.09/0.22 thf(f472,plain,(
% 0.09/0.22 ($true != ((sK6 @ (cP @ (cR @ (sK5 @ sK6)) @ (cR @ (sK4 @ sK6)))))) | (cZ != ((sK5 @ sK6))) | ~spl7_2),
% 0.09/0.22 inference(forward_subsumption_resolution,[],[f441,f117])).
% 0.09/0.22 thf(f473,plain,(
% 0.09/0.22 (cZ != ((sK5 @ sK6))) | (~spl7_2 | ~spl7_3)),
% 0.09/0.22 inference(forward_subsumption_resolution,[],[f472,f121])).
% 0.09/0.22 thf(f475,plain,(
% 0.09/0.22 (((sK6 @ (cP @ (cR @ sK3) @ (cR @ sK2)))) != $true) | ($true = ((sK6 @ (cP @ (sK5 @ sK6) @ cZ)))) | ~spl7_1),
% 0.09/0.22 inference(superposition,[],[f16,f114])).
% 0.09/0.22 thf(f476,plain,(
% 0.09/0.22 ($true = ((sK6 @ (cP @ (sK5 @ sK6) @ cZ)))) | (~spl7_1 | ~spl7_2)),
% 0.09/0.22 inference(forward_subsumption_resolution,[],[f475,f117])).
% 0.09/0.22 thf(f486,plain,(
% 0.09/0.22 (cZ = ((sK5 @ sK6))) | ($true = $false) | (~spl7_1 | ~spl7_2)),
% 0.09/0.22 inference(superposition,[],[f31,f476])).
% 0.09/0.22 thf(f496,plain,(
% 0.09/0.22 (cZ = ((sK5 @ sK6))) | (~spl7_1 | ~spl7_2)),
% 0.09/0.22 inference(trivial_inequality_removal,[],[f486])).
% 0.09/0.22 thf(f504,plain,(
% 0.09/0.22 $false | (~spl7_1 | ~spl7_2 | ~spl7_3)),
% 0.09/0.22 inference(forward_subsumption_resolution,[],[f496,f473])).
% 0.09/0.22 thf(f505,plain,(
% 0.09/0.22 ~spl7_1 | ~spl7_2 | ~spl7_3),
% 0.09/0.22 inference(avatar_contradiction_clause,[],[f504])).
% 0.09/0.22 cnf(s1, plain, spl7_1 | ~spl7_2 | ~spl7_3, inference(sat_conversion,[],[f123])).
% 0.09/0.22 cnf(s31, plain, spl7_2, inference(sat_conversion,[],[f440])).
% 0.09/0.22 cnf(s32, plain, ~spl7_2 | spl7_3, inference(sat_conversion,[],[f471])).
% 0.09/0.22 cnf(s35, plain, ~spl7_1 | ~spl7_2 | ~spl7_3, inference(sat_conversion,[],[f505])).
% 0.09/0.22 cnf(s36, plain, spl7_3, inference(rat,[],[s32,s31])).
% 0.09/0.22 cnf(s37, plain, ~spl7_1, inference(rat,[],[s35,s31,s36])).
% 0.09/0.22 cnf(s40, plain, $false, inference(rat,[],[s1,s36,s31,s37])).
% 0.09/0.22 thf(f506,plain,(
% 0.09/0.22 $false),
% 0.09/0.22 inference(avatar_sat_refutation,[],[s40])).
% 0.09/0.22 % SZS output end Proof for theBenchmark
% 0.09/0.22 % (212827)------------------------------
% 0.09/0.22 % (212827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.22 % (212827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.22 % (212827)CaDiCaL version: 2.1.3
% 0.09/0.22 % (212827)Termination reason: Refutation
% 0.09/0.22 % (212827)Time elapsed: 0.011 s
% 0.09/0.22 % (212827)Peak memory usage: 13 MB
% 0.09/0.22 % (212827)Instructions burned: 38 (million)
% 0.09/0.22 % (212769)Success in time 0.088 s
% 0.09/0.22 % Vampire exiting
%------------------------------------------------------------------------------