%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV149^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 : n001.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:37:54 AM UTC 2026
% Result : Theorem 0.88s 0.45s
% Output : Refutation 0.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV149^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 % Computer : n001.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Tue Sep 29 15:22:36 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.27 Running higher-order theorem proving
% 0.08/0.29 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.88/0.44 % (1376162)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.88/0.44 % (1376173)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.88/0.44 % (1376173)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.88/0.44 % (1376169)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3815860194:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.88/0.44 % (1376168)lrs+10_16_si=on:nwc=1.5:random_seed=747526269:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.88/0.44 % (1376167)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2725286394:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.88/0.44 % (1376172)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=622814520:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.88/0.44 % (1376173)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=2533306016:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.88/0.44 % (1376170)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=1155072803: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.88/0.44 % (1376171)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1571881857:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.88/0.44 % (1376169)Instruction limit reached!
% 0.88/0.44 % (1376169)------------------------------
% 0.88/0.44 % (1376169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.44 % (1376169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.44 % (1376169)CaDiCaL version: 2.1.3
% 0.88/0.44 % (1376169)Termination reason: Instruction limit
% 0.88/0.44 % (1376169)Termination phase: Saturation
% 0.88/0.44 % (1376169)Time elapsed: 0.004 s
% 0.88/0.44 % (1376169)Peak memory usage: 11 MB
% 0.88/0.44 % (1376169)Instructions burned: 3 (million)
% 0.88/0.44 % (1376168)Instruction limit reached!
% 0.88/0.44 % (1376168)------------------------------
% 0.88/0.44 % (1376168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.44 % (1376168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.44 % (1376168)CaDiCaL version: 2.1.3
% 0.88/0.44 % (1376168)Termination reason: Instruction limit
% 0.88/0.44 % (1376168)Termination phase: Saturation
% 0.88/0.44 % (1376168)Time elapsed: 0.018 s
% 0.88/0.44 % (1376168)Peak memory usage: 12 MB
% 0.88/0.44 % (1376168)Instructions burned: 18 (million)
% 0.88/0.44 % (1376171)Instruction limit reached!
% 0.88/0.44 % (1376171)------------------------------
% 0.88/0.44 % (1376171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.44 % (1376171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.44 % (1376171)CaDiCaL version: 2.1.3
% 0.88/0.44 % (1376171)Termination reason: Instruction limit
% 0.88/0.44 % (1376171)Termination phase: Saturation
% 0.88/0.44 % (1376171)Time elapsed: 0.029 s
% 0.88/0.44 % (1376171)Peak memory usage: 11 MB
% 0.88/0.44 % (1376171)Instructions burned: 27 (million)
% 0.88/0.44 % (1376181)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2653447014:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.88/0.44 % (1376181)Instruction limit reached!
% 0.88/0.44 % (1376181)------------------------------
% 0.88/0.44 % (1376181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.44 % (1376181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.44 % (1376181)CaDiCaL version: 2.1.3
% 0.88/0.44 % (1376181)Termination reason: Instruction limit
% 0.88/0.44 % (1376181)Termination phase: Saturation
% 0.88/0.44 % (1376181)Time elapsed: 0.003 s
% 0.88/0.44 % (1376181)Peak memory usage: 10 MB
% 0.88/0.44 % (1376181)Instructions burned: 2 (million)
% 0.88/0.44 % (1376183)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.88/0.44 % (1376183)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3894753438:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.88/0.44 % (1376182)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=4047692580:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.88/0.44 % (1376183)Instruction limit reached!
% 0.88/0.44 % (1376183)------------------------------
% 0.88/0.44 % (1376183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.44 % (1376183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.44 % (1376183)CaDiCaL version: 2.1.3
% 0.88/0.44 % (1376183)Termination reason: Instruction limit
% 0.88/0.44 % (1376183)Termination phase: Saturation
% 0.88/0.44 % (1376183)Time elapsed: 0.004 s
% 0.88/0.44 % (1376183)Peak memory usage: 12 MB
% 0.88/0.44 % (1376183)Instructions burned: 8 (million)
% 0.88/0.44 % (1376182)Instruction limit reached!
% 0.88/0.44 % (1376182)------------------------------
% 0.88/0.44 % (1376182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.44 % (1376182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.44 % (1376182)CaDiCaL version: 2.1.3
% 0.88/0.44 % (1376182)Termination reason: Instruction limit
% 0.88/0.44 % (1376182)Termination phase: Saturation
% 0.88/0.44 % (1376182)Time elapsed: 0.005 s
% 0.88/0.44 % (1376182)Peak memory usage: 11 MB
% 0.88/0.44 % (1376182)Instructions burned: 5 (million)
% 0.88/0.44 % (1376188)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.88/0.44 % (1376188)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.88/0.44 % (1376172)Instruction limit reached!
% 0.88/0.44 % (1376172)------------------------------
% 0.88/0.44 % (1376172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.44 % (1376172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.45 % (1376172)CaDiCaL version: 2.1.3
% 0.88/0.45 % (1376172)Termination reason: Instruction limit
% 0.88/0.45 % (1376172)Termination phase: Saturation
% 0.88/0.45 % (1376172)Time elapsed: 0.071 s
% 0.88/0.45 % (1376172)Peak memory usage: 13 MB
% 0.88/0.45 % (1376172)Instructions burned: 76 (million)
% 0.88/0.45 % (1376188)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3924905716: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.88/0.45 % (1376185)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=560431324:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.88/0.45 % (1376167)Instruction limit reached!
% 0.88/0.45 % (1376167)------------------------------
% 0.88/0.45 % (1376167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.45 % (1376167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.45 % (1376167)CaDiCaL version: 2.1.3
% 0.88/0.45 % (1376167)Termination reason: Instruction limit
% 0.88/0.45 % (1376167)Termination phase: Saturation
% 0.88/0.45 % (1376167)Time elapsed: 0.085 s
% 0.88/0.45 % (1376167)Peak memory usage: 12 MB
% 0.88/0.45 % (1376167)Instructions burned: 87 (million)
% 0.88/0.45 % (1376188)Instruction limit reached!
% 0.88/0.45 % (1376188)------------------------------
% 0.88/0.45 % (1376188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.45 % (1376188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.45 % (1376188)CaDiCaL version: 2.1.3
% 0.88/0.45 % (1376188)Termination reason: Instruction limit
% 0.88/0.45 % (1376188)Termination phase: Saturation
% 0.88/0.45 % (1376188)Time elapsed: 0.013 s
% 0.88/0.45 % (1376188)Peak memory usage: 12 MB
% 0.88/0.45 % (1376188)Instructions burned: 29 (million)
% 0.88/0.45 % (1376185)Instruction limit reached!
% 0.88/0.45 % (1376185)------------------------------
% 0.88/0.45 % (1376185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.45 % (1376185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.45 % (1376185)CaDiCaL version: 2.1.3
% 0.88/0.45 % (1376185)Termination reason: Instruction limit
% 0.88/0.45 % (1376185)Termination phase: Saturation
% 0.88/0.45 % (1376185)Time elapsed: 0.013 s
% 0.88/0.45 % (1376185)Peak memory usage: 12 MB
% 0.88/0.45 % (1376185)Instructions burned: 12 (million)
% 0.88/0.45 % (1376189)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=998264082:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.88/0.45 % (1376173) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1376162-1376173"...
% 0.88/0.45 % (1376193)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.88/0.45 % (1376193)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=2374334893:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 0.88/0.45 % (1376191)lrs+10_1_si=on:cs=on:random_seed=4117283458:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.88/0.45 % (1376173)...printing done.
% 0.88/0.45 % (1376193)Instruction limit reached!
% 0.88/0.45 % (1376193)------------------------------
% 0.88/0.45 % (1376193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.45 % (1376193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.45 % (1376193)CaDiCaL version: 2.1.3
% 0.88/0.45 % (1376193)Termination reason: Instruction limit
% 0.88/0.45 % (1376193)Termination phase: Saturation
% 0.88/0.45 % (1376193)Time elapsed: 0.004 s
% 0.88/0.45 % (1376193)Peak memory usage: 12 MB
% 0.88/0.45 % (1376193)Instructions burned: 7 (million)
% 0.88/0.45 % (1376173)Refutation found. Thanks to Tanya!
% 0.88/0.45 % SZS status Theorem for theBenchmark
% 0.88/0.45 % SZS output start Proof for theBenchmark
% 0.88/0.45 thf(type_def_5, type, a: $tType).
% 0.88/0.45 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.88/0.45 thf(func_def_3, type, sP0: ((a > a > $o) > (a > a > $o) > (a > $o) > $o)).
% 0.88/0.45 thf(func_def_4, type, sP1: (a > (a > a > $o) > a > $o)).
% 0.88/0.45 thf(func_def_5, type, sP2: (a > a > (a > a > $o) > $o)).
% 0.88/0.45 thf(func_def_6, type, sP3: (a > a > (a > a > $o) > $o)).
% 0.88/0.45 thf(func_def_7, type, sP4: (a > (a > a > $o) > a > $o)).
% 0.88/0.45 thf(func_def_8, type, sK5: (a > (a > a > $o) > a > a > $o)).
% 0.88/0.45 thf(func_def_9, type, sK6: (a > a > (a > a > $o) > a > $o)).
% 0.88/0.45 thf(func_def_10, type, sK7: (a > a > (a > a > $o) > a > $o)).
% 0.88/0.45 thf(func_def_11, type, sK8: (a > (a > a > $o) > a > a > $o)).
% 0.88/0.45 thf(func_def_12, type, sK9: ((a > a > $o) > (a > a > $o) > (a > $o) > a)).
% 0.88/0.45 thf(func_def_13, type, sK10: ((a > a > $o) > (a > a > $o) > (a > $o) > a)).
% 0.88/0.45 thf(func_def_14, type, sK11: (a > a > $o)).
% 0.88/0.45 thf(func_def_15, type, sK12: a).
% 0.88/0.45 thf(func_def_16, type, sK13: a).
% 0.88/0.45 thf(func_def_17, type, sK14: (a > a > $o)).
% 0.88/0.45 thf(func_def_18, type, sK15: (a > $o)).
% 0.88/0.45 thf(func_def_19, type, sK16: ((a > $o) > a)).
% 0.88/0.45 thf(func_def_20, type, sF17: (a > $o)).
% 0.88/0.45 thf(func_def_21, type, sF18: (a > $o)).
% 0.88/0.45 thf(func_def_22, type, sF19: (a > $o)).
% 0.88/0.45 thf(func_def_23, type, sF20: (a > a > $o)).
% 0.88/0.45 thf(func_def_24, type, sF21: (a > a > $o)).
% 0.88/0.45 thf(func_def_25, type, sF22: $o).
% 0.88/0.45 thf(func_def_26, type, sF23: ((a > $o) > $o)).
% 0.88/0.45 thf(func_def_27, type, sF24: ((a > $o) > $o)).
% 0.88/0.45 thf(func_def_28, type, sF25: ((a > $o) > a)).
% 0.88/0.45 thf(func_def_29, type, sF26: ((a > $o) > $o)).
% 0.88/0.45 thf(func_def_30, type, sF27: ((a > $o) > $o)).
% 0.88/0.45 thf(func_def_31, type, sF28: ((a > $o) > $o)).
% 0.88/0.45 thf(func_def_33, type, db0: !>[X0: $tType]:(X0)).
% 0.88/0.45 thf(func_def_34, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.88/0.45 thf(f1,conjecture,(
% 0.88/0.45 ! [X3 : a,X0 : (a > a > $o),X2 : a,X1 : (a > a > $o)] : (! [X4 : (a > $o)] : ((! [X5 : a] : (((X1 @ X2 @ X5) | (X0 @ X2 @ X5)) => (X4 @ X5)) & ! [X7 : a,X6 : a] : ((((X1 @ X6 @ X7) | (X0 @ X6 @ X7)) & (X4 @ X6)) => (X4 @ X7))) => (X4 @ X3)) => ! [X4 : (a > $o)] : ((! [X5 : a] : ((! [X8 : (a > $o)] : ((! [X6 : a,X7 : a] : (((X0 @ X6 @ X7) & (X8 @ X6)) => (X8 @ X7)) & ! [X9 : a] : ((X0 @ X2 @ X9) => (X8 @ X9))) => (X8 @ X5)) | ! [X8 : (a > $o)] : ((! [X9 : a] : ((X1 @ X2 @ X9) => (X8 @ X9)) & ! [X7 : a,X6 : a] : (((X8 @ X6) & (X1 @ X6 @ X7)) => (X8 @ X7))) => (X8 @ X5))) => (X4 @ X5)) & ! [X6 : a,X7 : a] : (((! [X8 : (a > $o)] : ((! [X10 : a,X11 : a] : (((X8 @ X10) & (X1 @ X10 @ X11)) => (X8 @ X11)) & ! [X5 : a] : ((X1 @ X6 @ X5) => (X8 @ X5))) => (X8 @ X7)) | ! [X8 : (a > $o)] : ((! [X5 : a] : ((X0 @ X6 @ X5) => (X8 @ X5)) & ! [X10 : a,X11 : a] : (((X0 @ X10 @ X11) & (X8 @ X10)) => (X8 @ X11))) => (X8 @ X7))) & (X4 @ X6)) => (X4 @ X7))) => (X4 @ X3)))),
% 0.88/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM251B_pme)).
% 0.88/0.45 thf(f2,negated_conjecture,(
% 0.88/0.45 ~ ! [X3 : a,X0 : (a > a > $o),X2 : a,X1 : (a > a > $o)] : (! [X4 : (a > $o)] : ((! [X5 : a] : (((X1 @ X2 @ X5) | (X0 @ X2 @ X5)) => (X4 @ X5)) & ! [X7 : a,X6 : a] : ((((X1 @ X6 @ X7) | (X0 @ X6 @ X7)) & (X4 @ X6)) => (X4 @ X7))) => (X4 @ X3)) => ! [X4 : (a > $o)] : ((! [X5 : a] : ((! [X8 : (a > $o)] : ((! [X6 : a,X7 : a] : (((X0 @ X6 @ X7) & (X8 @ X6)) => (X8 @ X7)) & ! [X9 : a] : ((X0 @ X2 @ X9) => (X8 @ X9))) => (X8 @ X5)) | ! [X8 : (a > $o)] : ((! [X9 : a] : ((X1 @ X2 @ X9) => (X8 @ X9)) & ! [X7 : a,X6 : a] : (((X8 @ X6) & (X1 @ X6 @ X7)) => (X8 @ X7))) => (X8 @ X5))) => (X4 @ X5)) & ! [X6 : a,X7 : a] : (((! [X8 : (a > $o)] : ((! [X10 : a,X11 : a] : (((X8 @ X10) & (X1 @ X10 @ X11)) => (X8 @ X11)) & ! [X5 : a] : ((X1 @ X6 @ X5) => (X8 @ X5))) => (X8 @ X7)) | ! [X8 : (a > $o)] : ((! [X5 : a] : ((X0 @ X6 @ X5) => (X8 @ X5)) & ! [X10 : a,X11 : a] : (((X0 @ X10 @ X11) & (X8 @ X10)) => (X8 @ X11))) => (X8 @ X7))) & (X4 @ X6)) => (X4 @ X7))) => (X4 @ X3)))),
% 0.88/0.45 inference(negated_conjecture,[status(cth)],[f1])).
% 0.88/0.45 thf(f3,plain,(
% 0.88/0.45 ~ ! [X0 : a,X1 : (a > a > $o),X2 : a,X3 : (a > a > $o)] : (! [X4 : (a > $o)] : ((! [X5 : a] : (((X3 @ X2 @ X5) | (X1 @ X2 @ X5)) => (X4 @ X5)) & ! [X6 : a,X7 : a] : ((((X3 @ X7 @ X6) | (X1 @ X7 @ X6)) & (X4 @ X7)) => (X4 @ X6))) => (X4 @ X0)) => ! [X8 : (a > $o)] : ((! [X9 : a] : ((! [X10 : (a > $o)] : ((! [X11 : a,X12 : a] : (((X1 @ X11 @ X12) & (X10 @ X11)) => (X10 @ X12)) & ! [X13 : a] : ((X1 @ X2 @ X13) => (X10 @ X13))) => (X10 @ X9)) | ! [X14 : (a > $o)] : ((! [X15 : a] : ((X3 @ X2 @ X15) => (X14 @ X15)) & ! [X16 : a,X17 : a] : (((X14 @ X17) & (X3 @ X17 @ X16)) => (X14 @ X16))) => (X14 @ X9))) => (X8 @ X9)) & ! [X18 : a,X19 : a] : (((! [X20 : (a > $o)] : ((! [X21 : a,X22 : a] : (((X20 @ X21) & (X3 @ X21 @ X22)) => (X20 @ X22)) & ! [X23 : a] : ((X3 @ X18 @ X23) => (X20 @ X23))) => (X20 @ X19)) | ! [X24 : (a > $o)] : ((! [X25 : a] : ((X1 @ X18 @ X25) => (X24 @ X25)) & ! [X26 : a,X27 : a] : (((X1 @ X26 @ X27) & (X24 @ X26)) => (X24 @ X27))) => (X24 @ X19))) & (X8 @ X18)) => (X8 @ X19))) => (X8 @ X0)))),
% 0.88/0.45 inference(rectify,[],[f2])).
% 0.88/0.45 thf(f4,plain,(
% 0.88/0.45 ~ ! [X1 : (a > a > $o),X2 : a,X0 : a,X3 : (a > a > $o)] : (! [X4 : (a > $o)] : ((! [X5 : a] : (((((X1 @ X2 @ X5)) = $true) | (((X3 @ X2 @ X5)) = $true)) => (((X4 @ X5)) = $true)) & ! [X6 : a,X7 : a] : ((((((X3 @ X7 @ X6)) = $true) | (((X1 @ X7 @ X6)) = $true)) & (((X4 @ X7)) = $true)) => (((X4 @ X6)) = $true))) => (((X4 @ X0)) = $true)) => ! [X8 : (a > $o)] : ((! [X9 : a] : ((! [X14 : (a > $o)] : ((! [X17 : a,X16 : a] : (((((X14 @ X17)) = $true) & (((X3 @ X17 @ X16)) = $true)) => (((X14 @ X16)) = $true)) & ! [X15 : a] : ((((X3 @ X2 @ X15)) = $true) => (((X14 @ X15)) = $true))) => (((X14 @ X9)) = $true)) | ! [X10 : (a > $o)] : ((! [X13 : a] : ((((X1 @ X2 @ X13)) = $true) => (((X10 @ X13)) = $true)) & ! [X12 : a,X11 : a] : (((((X1 @ X11 @ X12)) = $true) & (((X10 @ X11)) = $true)) => (((X10 @ X12)) = $true))) => (((X10 @ X9)) = $true))) => (((X8 @ X9)) = $true)) & ! [X19 : a,X18 : a] : (((((X8 @ X18)) = $true) & (! [X20 : (a > $o)] : ((! [X22 : a,X21 : a] : (((((X20 @ X21)) = $true) & (((X3 @ X21 @ X22)) = $true)) => (((X20 @ X22)) = $true)) & ! [X23 : a] : ((((X3 @ X18 @ X23)) = $true) => (((X20 @ X23)) = $true))) => (((X20 @ X19)) = $true)) | ! [X24 : (a > $o)] : ((! [X27 : a,X26 : a] : (((((X1 @ X26 @ X27)) = $true) & (((X24 @ X26)) = $true)) => (((X24 @ X27)) = $true)) & ! [X25 : a] : ((((X1 @ X18 @ X25)) = $true) => (((X24 @ X25)) = $true))) => (((X24 @ X19)) = $true)))) => (((X8 @ X19)) = $true))) => (((X8 @ X0)) = $true)))),
% 0.88/0.45 inference(fool_elimination,[],[f3])).
% 0.88/0.45 thf(f5,plain,(
% 0.88/0.45 ? [X1 : (a > a > $o),X2 : a,X0 : a,X3 : (a > a > $o)] : (? [X8 : (a > $o)] : ((((X8 @ X0)) != $true) & (! [X9 : a] : ((((X8 @ X9)) = $true) | (? [X14 : (a > $o)] : ((((X14 @ X9)) != $true) & (! [X17 : a,X16 : a] : ((((X14 @ X16)) = $true) | ((((X14 @ X17)) != $true) | (((X3 @ X17 @ X16)) != $true))) & ! [X15 : a] : ((((X14 @ X15)) = $true) | (((X3 @ X2 @ X15)) != $true)))) & ? [X10 : (a > $o)] : ((((X10 @ X9)) != $true) & (! [X13 : a] : ((((X10 @ X13)) = $true) | (((X1 @ X2 @ X13)) != $true)) & ! [X12 : a,X11 : a] : ((((X10 @ X12)) = $true) | ((((X1 @ X11 @ X12)) != $true) | (((X10 @ X11)) != $true))))))) & ! [X19 : a,X18 : a] : ((((X8 @ X19)) = $true) | ((((X8 @ X18)) != $true) | (? [X20 : (a > $o)] : ((((X20 @ X19)) != $true) & (! [X22 : a,X21 : a] : ((((X20 @ X22)) = $true) | ((((X20 @ X21)) != $true) | (((X3 @ X21 @ X22)) != $true))) & ! [X23 : a] : ((((X3 @ X18 @ X23)) != $true) | (((X20 @ X23)) = $true)))) & ? [X24 : (a > $o)] : ((((X24 @ X19)) != $true) & (! [X27 : a,X26 : a] : ((((X24 @ X27)) = $true) | ((((X1 @ X26 @ X27)) != $true) | (((X24 @ X26)) != $true))) & ! [X25 : a] : ((((X24 @ X25)) = $true) | (((X1 @ X18 @ X25)) != $true))))))))) & ! [X4 : (a > $o)] : ((((X4 @ X0)) = $true) | (? [X5 : a] : (((((X1 @ X2 @ X5)) = $true) | (((X3 @ X2 @ X5)) = $true)) & (((X4 @ X5)) != $true)) | ? [X6 : a,X7 : a] : ((((X4 @ X6)) != $true) & (((((X3 @ X7 @ X6)) = $true) | (((X1 @ X7 @ X6)) = $true)) & (((X4 @ X7)) = $true))))))),
% 0.88/0.45 inference(ennf_transformation,[],[f4])).
% 0.88/0.45 thf(f6,plain,(
% 0.88/0.45 ? [X1 : (a > a > $o),X0 : a,X2 : a,X3 : (a > a > $o)] : (? [X8 : (a > $o)] : (! [X9 : a] : ((? [X10 : (a > $o)] : (! [X13 : a] : ((((X10 @ X13)) = $true) | (((X1 @ X2 @ X13)) != $true)) & ! [X12 : a,X11 : a] : ((((X10 @ X11)) != $true) | (((X1 @ X11 @ X12)) != $true) | (((X10 @ X12)) = $true)) & (((X10 @ X9)) != $true)) & ? [X14 : (a > $o)] : (! [X16 : a,X17 : a] : ((((X14 @ X16)) = $true) | (((X3 @ X17 @ X16)) != $true) | (((X14 @ X17)) != $true)) & ! [X15 : a] : ((((X14 @ X15)) = $true) | (((X3 @ X2 @ X15)) != $true)) & (((X14 @ X9)) != $true))) | (((X8 @ X9)) = $true)) & ! [X18 : a,X19 : a] : ((((X8 @ X18)) != $true) | (? [X20 : (a > $o)] : (! [X22 : a,X21 : a] : ((((X20 @ X21)) != $true) | (((X3 @ X21 @ X22)) != $true) | (((X20 @ X22)) = $true)) & ! [X23 : a] : ((((X3 @ X18 @ X23)) != $true) | (((X20 @ X23)) = $true)) & (((X20 @ X19)) != $true)) & ? [X24 : (a > $o)] : (! [X25 : a] : ((((X24 @ X25)) = $true) | (((X1 @ X18 @ X25)) != $true)) & (((X24 @ X19)) != $true) & ! [X27 : a,X26 : a] : ((((X24 @ X27)) = $true) | (((X24 @ X26)) != $true) | (((X1 @ X26 @ X27)) != $true)))) | (((X8 @ X19)) = $true)) & (((X8 @ X0)) != $true)) & ! [X4 : (a > $o)] : ((((X4 @ X0)) = $true) | ? [X6 : a,X7 : a] : ((((X4 @ X7)) = $true) & ((((X3 @ X7 @ X6)) = $true) | (((X1 @ X7 @ X6)) = $true)) & (((X4 @ X6)) != $true)) | ? [X5 : a] : (((((X1 @ X2 @ X5)) = $true) | (((X3 @ X2 @ X5)) = $true)) & (((X4 @ X5)) != $true))))),
% 0.88/0.45 inference(flattening,[],[f5])).
% 0.88/0.45 thf(f7,definition,(
% 0.88/0.45 ! [X4 : (a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (? [X6 : a,X7 : a] : ((((X4 @ X7)) = $true) & ((((X3 @ X7 @ X6)) = $true) | (((X1 @ X7 @ X6)) = $true)) & (((X4 @ X6)) != $true)) | ~ ($true = ((sP0 @ X1 @ X3 @ X4))))),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 0.88/0.45 thf(f8,definition,(
% 0.88/0.45 ! [X18 : a,X1 : (a > a > $o),X19 : a] : (? [X24 : (a > $o)] : (! [X25 : a] : ((((X24 @ X25)) = $true) | (((X1 @ X18 @ X25)) != $true)) & (((X24 @ X19)) != $true) & ! [X27 : a,X26 : a] : ((((X24 @ X27)) = $true) | (((X24 @ X26)) != $true) | (((X1 @ X26 @ X27)) != $true))) | ~ (((sP1 @ X19 @ X1 @ X18)) = $true))),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 0.88/0.45 thf(f9,definition,(
% 0.88/0.45 ! [X3 : (a > a > $o),X18 : a,X19 : a] : (? [X20 : (a > $o)] : (! [X22 : a,X21 : a] : ((((X20 @ X21)) != $true) | (((X3 @ X21 @ X22)) != $true) | (((X20 @ X22)) = $true)) & ! [X23 : a] : ((((X3 @ X18 @ X23)) != $true) | (((X20 @ X23)) = $true)) & (((X20 @ X19)) != $true)) | ~ (((sP2 @ X19 @ X18 @ X3)) = $true))),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 0.88/0.45 thf(f10,definition,(
% 0.88/0.45 ! [X3 : (a > a > $o),X2 : a,X9 : a] : (? [X14 : (a > $o)] : (! [X16 : a,X17 : a] : ((((X14 @ X16)) = $true) | (((X3 @ X17 @ X16)) != $true) | (((X14 @ X17)) != $true)) & ! [X15 : a] : ((((X14 @ X15)) = $true) | (((X3 @ X2 @ X15)) != $true)) & (((X14 @ X9)) != $true)) | ~ ($true = ((sP3 @ X9 @ X2 @ X3))))),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 0.88/0.45 thf(f11,definition,(
% 0.88/0.45 ! [X2 : a,X1 : (a > a > $o),X9 : a] : (? [X10 : (a > $o)] : (! [X13 : a] : ((((X10 @ X13)) = $true) | (((X1 @ X2 @ X13)) != $true)) & ! [X12 : a,X11 : a] : ((((X10 @ X11)) != $true) | (((X1 @ X11 @ X12)) != $true) | (((X10 @ X12)) = $true)) & (((X10 @ X9)) != $true)) | ~ (((sP4 @ X9 @ X1 @ X2)) = $true))),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 0.88/0.45 thf(f12,plain,(
% 0.88/0.45 ? [X1 : (a > a > $o),X0 : a,X2 : a,X3 : (a > a > $o)] : (? [X8 : (a > $o)] : (! [X9 : a] : (((((sP4 @ X9 @ X1 @ X2)) = $true) & ($true = ((sP3 @ X9 @ X2 @ X3)))) | (((X8 @ X9)) = $true)) & ! [X18 : a,X19 : a] : ((((X8 @ X18)) != $true) | ((((sP2 @ X19 @ X18 @ X3)) = $true) & (((sP1 @ X19 @ X1 @ X18)) = $true)) | (((X8 @ X19)) = $true)) & (((X8 @ X0)) != $true)) & ! [X4 : (a > $o)] : ((((X4 @ X0)) = $true) | ($true = ((sP0 @ X1 @ X3 @ X4))) | ? [X5 : a] : (((((X1 @ X2 @ X5)) = $true) | (((X3 @ X2 @ X5)) = $true)) & (((X4 @ X5)) != $true))))),
% 0.88/0.45 inference(definition_folding,[],[f6,f11,f10,f9,f8,f7])).
% 0.88/0.45 thf(f13,plain,(
% 0.88/0.45 ! [X2 : a,X1 : (a > a > $o),X9 : a] : (? [X10 : (a > $o)] : (! [X13 : a] : ((((X10 @ X13)) = $true) | (((X1 @ X2 @ X13)) != $true)) & ! [X12 : a,X11 : a] : ((((X10 @ X11)) != $true) | (((X1 @ X11 @ X12)) != $true) | (((X10 @ X12)) = $true)) & (((X10 @ X9)) != $true)) | (((sP4 @ X9 @ X1 @ X2)) != $true))),
% 0.88/0.45 inference(nnf_transformation,[],[f11])).
% 0.88/0.45 thf(f14,plain,(
% 0.88/0.45 ! [X0 : a,X1 : (a > a > $o),X2 : a] : (? [X3 : (a > $o)] : (! [X4 : a] : ((((X3 @ X4)) = $true) | (((X1 @ X0 @ X4)) != $true)) & ! [X5 : a,X6 : a] : ((((X3 @ X6)) != $true) | (((X1 @ X6 @ X5)) != $true) | (((X3 @ X5)) = $true)) & (((X3 @ X2)) != $true)) | (((sP4 @ X2 @ X1 @ X0)) != $true))),
% 0.88/0.45 inference(rectify,[],[f13])).
% 0.88/0.45 thf(f15,plain,(
% 0.88/0.45 ! [X0 : a,X1 : (a > a > $o),X2 : a] : ((! [X4 : a] : ((((sK5 @ X2 @ X1 @ X0 @ X4)) = $true) | (((X1 @ X0 @ X4)) != $true)) & ! [X5 : a,X6 : a] : ((((sK5 @ X2 @ X1 @ X0 @ X6)) != $true) | (((X1 @ X6 @ X5)) != $true) | (((sK5 @ X2 @ X1 @ X0 @ X5)) = $true)) & (((sK5 @ X2 @ X1 @ X0 @ X2)) != $true)) | (((sP4 @ X2 @ X1 @ X0)) != $true))),
% 0.88/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X3,sK5 @ X2 @ X1 @ X0)],[f14])).
% 0.88/0.45 thf(f16,plain,(
% 0.88/0.45 ! [X3 : (a > a > $o),X2 : a,X9 : a] : (? [X14 : (a > $o)] : (! [X16 : a,X17 : a] : ((((X14 @ X16)) = $true) | (((X3 @ X17 @ X16)) != $true) | (((X14 @ X17)) != $true)) & ! [X15 : a] : ((((X14 @ X15)) = $true) | (((X3 @ X2 @ X15)) != $true)) & (((X14 @ X9)) != $true)) | ($true != ((sP3 @ X9 @ X2 @ X3))))),
% 0.88/0.45 inference(nnf_transformation,[],[f10])).
% 0.88/0.45 thf(f17,plain,(
% 0.88/0.45 ! [X0 : (a > a > $o),X1 : a,X2 : a] : (? [X3 : (a > $o)] : (! [X4 : a,X5 : a] : ((((X3 @ X4)) = $true) | (((X0 @ X5 @ X4)) != $true) | (((X3 @ X5)) != $true)) & ! [X6 : a] : ((((X3 @ X6)) = $true) | (((X0 @ X1 @ X6)) != $true)) & (((X3 @ X2)) != $true)) | (((sP3 @ X2 @ X1 @ X0)) != $true))),
% 0.88/0.45 inference(rectify,[],[f16])).
% 0.88/0.45 thf(f18,plain,(
% 0.88/0.45 ! [X0 : (a > a > $o),X1 : a,X2 : a] : ((! [X4 : a,X5 : a] : ((((sK6 @ X2 @ X1 @ X0 @ X4)) = $true) | (((X0 @ X5 @ X4)) != $true) | (((sK6 @ X2 @ X1 @ X0 @ X5)) != $true)) & ! [X6 : a] : ((((sK6 @ X2 @ X1 @ X0 @ X6)) = $true) | (((X0 @ X1 @ X6)) != $true)) & (((sK6 @ X2 @ X1 @ X0 @ X2)) != $true)) | (((sP3 @ X2 @ X1 @ X0)) != $true))),
% 0.88/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X3,sK5 @ X2 @ X1 @ X0)],[f17])).
% 0.88/0.45 thf(f19,plain,(
% 0.88/0.45 ! [X3 : (a > a > $o),X18 : a,X19 : a] : (? [X20 : (a > $o)] : (! [X22 : a,X21 : a] : ((((X20 @ X21)) != $true) | (((X3 @ X21 @ X22)) != $true) | (((X20 @ X22)) = $true)) & ! [X23 : a] : ((((X3 @ X18 @ X23)) != $true) | (((X20 @ X23)) = $true)) & (((X20 @ X19)) != $true)) | (((sP2 @ X19 @ X18 @ X3)) != $true))),
% 0.88/0.45 inference(nnf_transformation,[],[f9])).
% 0.88/0.45 thf(f20,plain,(
% 0.88/0.45 ! [X0 : (a > a > $o),X1 : a,X2 : a] : (? [X3 : (a > $o)] : (! [X4 : a,X5 : a] : ((((X3 @ X5)) != $true) | (((X0 @ X5 @ X4)) != $true) | (((X3 @ X4)) = $true)) & ! [X6 : a] : ((((X0 @ X1 @ X6)) != $true) | (((X3 @ X6)) = $true)) & (((X3 @ X2)) != $true)) | (((sP2 @ X2 @ X1 @ X0)) != $true))),
% 0.88/0.45 inference(rectify,[],[f19])).
% 0.88/0.45 thf(f21,plain,(
% 0.88/0.45 ! [X0 : (a > a > $o),X1 : a,X2 : a] : ((! [X4 : a,X5 : a] : ((((sK7 @ X2 @ X1 @ X0 @ X5)) != $true) | (((X0 @ X5 @ X4)) != $true) | (((sK7 @ X2 @ X1 @ X0 @ X4)) = $true)) & ! [X6 : a] : ((((X0 @ X1 @ X6)) != $true) | (((sK7 @ X2 @ X1 @ X0 @ X6)) = $true)) & (((sK7 @ X2 @ X1 @ X0 @ X2)) != $true)) | (((sP2 @ X2 @ X1 @ X0)) != $true))),
% 0.88/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X3,sK5 @ X2 @ X1 @ X0)],[f20])).
% 0.88/0.45 thf(f22,plain,(
% 0.88/0.45 ! [X18 : a,X1 : (a > a > $o),X19 : a] : (? [X24 : (a > $o)] : (! [X25 : a] : ((((X24 @ X25)) = $true) | (((X1 @ X18 @ X25)) != $true)) & (((X24 @ X19)) != $true) & ! [X27 : a,X26 : a] : ((((X24 @ X27)) = $true) | (((X24 @ X26)) != $true) | (((X1 @ X26 @ X27)) != $true))) | (((sP1 @ X19 @ X1 @ X18)) != $true))),
% 0.88/0.45 inference(nnf_transformation,[],[f8])).
% 0.88/0.45 thf(f23,plain,(
% 0.88/0.45 ! [X0 : a,X1 : (a > a > $o),X2 : a] : (? [X3 : (a > $o)] : (! [X4 : a] : ((((X3 @ X4)) = $true) | (((X1 @ X0 @ X4)) != $true)) & (((X3 @ X2)) != $true) & ! [X5 : a,X6 : a] : ((((X3 @ X5)) = $true) | (((X3 @ X6)) != $true) | (((X1 @ X6 @ X5)) != $true))) | (((sP1 @ X2 @ X1 @ X0)) != $true))),
% 0.88/0.45 inference(rectify,[],[f22])).
% 0.88/0.45 thf(f24,plain,(
% 0.88/0.45 ! [X0 : a,X1 : (a > a > $o),X2 : a] : ((! [X4 : a] : (($true = ((sK8 @ X2 @ X1 @ X0 @ X4))) | (((X1 @ X0 @ X4)) != $true)) & (((sK8 @ X2 @ X1 @ X0 @ X2)) != $true) & ! [X5 : a,X6 : a] : ((((sK8 @ X2 @ X1 @ X0 @ X5)) = $true) | (((sK8 @ X2 @ X1 @ X0 @ X6)) != $true) | (((X1 @ X6 @ X5)) != $true))) | (((sP1 @ X2 @ X1 @ X0)) != $true))),
% 0.88/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X3,sK5 @ X2 @ X1 @ X0)],[f23])).
% 0.88/0.45 thf(f25,plain,(
% 0.88/0.45 ! [X4 : (a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (? [X6 : a,X7 : a] : ((((X4 @ X7)) = $true) & ((((X3 @ X7 @ X6)) = $true) | (((X1 @ X7 @ X6)) = $true)) & (((X4 @ X6)) != $true)) | ($true != ((sP0 @ X1 @ X3 @ X4))))),
% 0.88/0.45 inference(nnf_transformation,[],[f7])).
% 0.88/0.45 thf(f26,plain,(
% 0.88/0.45 ! [X0 : (a > $o),X1 : (a > a > $o),X2 : (a > a > $o)] : (? [X3 : a,X4 : a] : ((((X0 @ X4)) = $true) & ((((X1 @ X4 @ X3)) = $true) | (((X2 @ X4 @ X3)) = $true)) & (((X0 @ X3)) != $true)) | (((sP0 @ X2 @ X1 @ X0)) != $true))),
% 0.88/0.45 inference(rectify,[],[f25])).
% 0.88/0.45 thf(f27,plain,(
% 0.88/0.45 ! [X0 : (a > $o),X1 : (a > a > $o),X2 : (a > a > $o)] : ((($true = ((X0 @ (sK10 @ X2 @ X1 @ X0)))) & (($true = ((X1 @ (sK10 @ X2 @ X1 @ X0) @ (sK9 @ X2 @ X1 @ X0)))) | (((X2 @ (sK10 @ X2 @ X1 @ X0) @ (sK9 @ X2 @ X1 @ X0))) = $true)) & (((X0 @ (sK9 @ X2 @ X1 @ X0))) != $true)) | (((sP0 @ X2 @ X1 @ X0)) != $true))),
% 0.88/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X3,sK5 @ X2 @ X1 @ X0),skolemize(X3,sK5 @ X2 @ X1 @ X0)],[f26])).
% 0.88/0.45 thf(f28,plain,(
% 0.88/0.45 ? [X0 : (a > a > $o),X1 : a,X2 : a,X3 : (a > a > $o)] : (? [X4 : (a > $o)] : (! [X5 : a] : (((((sP4 @ X5 @ X0 @ X2)) = $true) & (((sP3 @ X5 @ X2 @ X3)) = $true)) | (((X4 @ X5)) = $true)) & ! [X6 : a,X7 : a] : ((((X4 @ X6)) != $true) | ((((sP2 @ X7 @ X6 @ X3)) = $true) & ($true = ((sP1 @ X7 @ X0 @ X6)))) | (((X4 @ X7)) = $true)) & (((X4 @ X1)) != $true)) & ! [X8 : (a > $o)] : ((((X8 @ X1)) = $true) | (((sP0 @ X0 @ X3 @ X8)) = $true) | ? [X9 : a] : (((((X0 @ X2 @ X9)) = $true) | (((X3 @ X2 @ X9)) = $true)) & (((X8 @ X9)) != $true))))),
% 0.88/0.45 inference(rectify,[],[f12])).
% 0.88/0.45 thf(f29,plain,(
% 0.88/0.45 (! [X5 : a] : (((((sP4 @ X5 @ sK11 @ sK13)) = $true) & ($true = ((sP3 @ X5 @ sK13 @ sK14)))) | (((sK15 @ X5)) = $true)) & ! [X6 : a,X7 : a] : ((((sK15 @ X6)) != $true) | ((((sP2 @ X7 @ X6 @ sK14)) = $true) & ($true = ((sP1 @ X7 @ sK11 @ X6)))) | (((sK15 @ X7)) = $true)) & (((sK15 @ sK12)) != $true)) & ! [X8 : (a > $o)] : ((((X8 @ sK12)) = $true) | (((sP0 @ sK11 @ sK14 @ X8)) = $true) | (((((sK11 @ sK13 @ (sK16 @ X8))) = $true) | (((sK14 @ sK13 @ (sK16 @ X8))) = $true)) & (((X8 @ (sK16 @ X8))) != $true)))),
% 0.88/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13,sK14,sK15,vAPP]),skolemize(X0,sK11),skolemize(X1,sK12),skolemize(X2,sK13),skolemize(X3,sK14),skolemize(X4,sK15),skolemize(X3,sK5 @ X2 @ X1 @ X0)],[f28])).
% 0.88/0.45 thf(f30,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : a,X1 : (a > a > $o)] : ((((sK5 @ X2 @ X1 @ X0 @ X2)) != $true) | (((sP4 @ X2 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f15])).
% 0.88/0.45 thf(f32,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : a,X1 : (a > a > $o),X4 : a] : ((((sK5 @ X2 @ X1 @ X0 @ X4)) = $true) | (((X1 @ X0 @ X4)) != $true) | (((sP4 @ X2 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f15])).
% 0.88/0.45 thf(f33,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : (a > a > $o),X1 : a] : ((((sK6 @ X2 @ X1 @ X0 @ X2)) != $true) | (((sP3 @ X2 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f18])).
% 0.88/0.45 thf(f34,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : (a > a > $o),X1 : a,X6 : a] : ((((sK6 @ X2 @ X1 @ X0 @ X6)) = $true) | (((X0 @ X1 @ X6)) != $true) | (((sP3 @ X2 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f18])).
% 0.88/0.45 thf(f36,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : (a > a > $o),X1 : a] : ((((sK7 @ X2 @ X1 @ X0 @ X2)) != $true) | (((sP2 @ X2 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f21])).
% 0.88/0.45 thf(f37,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : (a > a > $o),X1 : a,X6 : a] : ((((sK7 @ X2 @ X1 @ X0 @ X6)) = $true) | (((X0 @ X1 @ X6)) != $true) | (((sP2 @ X2 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f21])).
% 0.88/0.45 thf(f40,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : a,X1 : (a > a > $o)] : ((((sK8 @ X2 @ X1 @ X0 @ X2)) != $true) | (((sP1 @ X2 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f24])).
% 0.88/0.45 thf(f41,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : a,X1 : (a > a > $o),X4 : a] : (($true = ((sK8 @ X2 @ X1 @ X0 @ X4))) | (((X1 @ X0 @ X4)) != $true) | (((sP1 @ X2 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f24])).
% 0.88/0.45 thf(f42,plain,(
% 0.88/0.45 ( ! [X2 : (a > a > $o),X0 : (a > $o),X1 : (a > a > $o)] : ((((X0 @ (sK9 @ X2 @ X1 @ X0))) != $true) | (((sP0 @ X2 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f27])).
% 0.88/0.45 thf(f43,plain,(
% 0.88/0.45 ( ! [X2 : (a > a > $o),X0 : (a > $o),X1 : (a > a > $o)] : (($true = ((X1 @ (sK10 @ X2 @ X1 @ X0) @ (sK9 @ X2 @ X1 @ X0)))) | (((sP0 @ X2 @ X1 @ X0)) != $true) | (((X2 @ (sK10 @ X2 @ X1 @ X0) @ (sK9 @ X2 @ X1 @ X0))) = $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f27])).
% 0.88/0.45 thf(f44,plain,(
% 0.88/0.45 ( ! [X2 : (a > a > $o),X0 : (a > $o),X1 : (a > a > $o)] : (($true = ((X0 @ (sK10 @ X2 @ X1 @ X0)))) | (((sP0 @ X2 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f27])).
% 0.88/0.45 thf(f45,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((X8 @ sK12)) = $true) | (((sP0 @ sK11 @ sK14 @ X8)) = $true) | (((X8 @ (sK16 @ X8))) != $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f29])).
% 0.88/0.45 thf(f46,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((X8 @ sK12)) = $true) | (((sP0 @ sK11 @ sK14 @ X8)) = $true) | (((sK11 @ sK13 @ (sK16 @ X8))) = $true) | (((sK14 @ sK13 @ (sK16 @ X8))) = $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f29])).
% 0.88/0.45 thf(f47,plain,(
% 0.88/0.45 (((sK15 @ sK12)) != $true)),
% 0.88/0.45 inference(cnf_transformation,[],[f29])).
% 0.88/0.45 thf(f48,plain,(
% 0.88/0.45 ( ! [X6 : a,X7 : a] : ((((sK15 @ X6)) != $true) | ($true = ((sP1 @ X7 @ sK11 @ X6))) | (((sK15 @ X7)) = $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f29])).
% 0.88/0.45 thf(f49,plain,(
% 0.88/0.45 ( ! [X6 : a,X7 : a] : ((((sK15 @ X6)) != $true) | (((sP2 @ X7 @ X6 @ sK14)) = $true) | (((sK15 @ X7)) = $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f29])).
% 0.88/0.45 thf(f50,plain,(
% 0.88/0.45 ( ! [X5 : a] : (($true = ((sP3 @ X5 @ sK13 @ sK14))) | (((sK15 @ X5)) = $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f29])).
% 0.88/0.45 thf(f51,plain,(
% 0.88/0.45 ( ! [X5 : a] : ((((sP4 @ X5 @ sK11 @ sK13)) = $true) | (((sK15 @ X5)) = $true)) )),
% 0.88/0.45 inference(cnf_transformation,[],[f29])).
% 0.88/0.45 thf(f53,definition,(
% 0.88/0.45 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.88/0.45 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.88/0.45 thf(f54,definition,(
% 0.88/0.45 ( ! [X5 : a] : ((((sF17 @ X5)) = ((sP4 @ X5 @ sK11 @ sK13)))) )),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 0.88/0.45 thf(f55,plain,(
% 0.88/0.45 ( ! [X5 : a] : ((((sP4 @ X5 @ sK11 @ sK13)) = ((sF17 @ X5)))) )),
% 0.88/0.45 inference(reorient_equations,[],[f54])).
% 0.88/0.45 thf(f56,definition,(
% 0.88/0.45 ( ! [X5 : a] : ((((sF18 @ X5)) = ((sK15 @ X5)))) )),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[sF18])],[function_definition])).
% 0.88/0.45 thf(f57,plain,(
% 0.88/0.45 ( ! [X5 : a] : ((((sK15 @ X5)) = ((sF18 @ X5)))) )),
% 0.88/0.45 inference(reorient_equations,[],[f56])).
% 0.88/0.45 thf(f58,plain,(
% 0.88/0.45 ( ! [X5 : a] : ((((sF18 @ X5)) = $true) | (((sF17 @ X5)) = $true)) )),
% 0.88/0.45 inference(definition_folding,[],[f51,f57,f55])).
% 0.88/0.45 thf(f59,definition,(
% 0.88/0.45 ( ! [X5 : a] : ((((sF19 @ X5)) = ((sP3 @ X5 @ sK13 @ sK14)))) )),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[sF19])],[function_definition])).
% 0.88/0.45 thf(f60,plain,(
% 0.88/0.45 ( ! [X5 : a] : ((((sF19 @ X5)) = $true) | (((sF18 @ X5)) = $true)) )),
% 0.88/0.45 inference(definition_folding,[],[f50,f57,f59])).
% 0.88/0.45 thf(f61,definition,(
% 0.88/0.45 ( ! [X6 : a,X7 : a] : ((((sF20 @ X6 @ X7)) = ((sP2 @ X7 @ X6 @ sK14)))) )),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[sF20])],[function_definition])).
% 0.88/0.45 thf(f62,plain,(
% 0.88/0.45 ( ! [X6 : a,X7 : a] : ((((sP2 @ X7 @ X6 @ sK14)) = ((sF20 @ X6 @ X7)))) )),
% 0.88/0.45 inference(reorient_equations,[],[f61])).
% 0.88/0.45 thf(f63,plain,(
% 0.88/0.45 ( ! [X6 : a,X7 : a] : ((((sF20 @ X6 @ X7)) = $true) | (((sF18 @ X6)) != $true) | (((sF18 @ X7)) = $true)) )),
% 0.88/0.45 inference(definition_folding,[],[f49,f57,f62,f57])).
% 0.88/0.45 thf(f64,definition,(
% 0.88/0.45 ( ! [X6 : a,X7 : a] : ((((sF21 @ X6 @ X7)) = ((sP1 @ X7 @ sK11 @ X6)))) )),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[sF21])],[function_definition])).
% 0.88/0.45 thf(f65,plain,(
% 0.88/0.45 ( ! [X6 : a,X7 : a] : ((((sF21 @ X6 @ X7)) = $true) | (((sF18 @ X7)) = $true) | (((sF18 @ X6)) != $true)) )),
% 0.88/0.45 inference(definition_folding,[],[f48,f57,f64,f57])).
% 0.88/0.45 thf(f66,definition,(
% 0.88/0.45 (sF22 = ((sK15 @ sK12)))),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[sF22])],[function_definition])).
% 0.88/0.45 thf(f67,plain,(
% 0.88/0.45 (((sK15 @ sK12)) = sF22)),
% 0.88/0.45 inference(reorient_equations,[],[f66])).
% 0.88/0.45 thf(f68,plain,(
% 0.88/0.45 (sF22 != $true)),
% 0.88/0.45 inference(definition_folding,[],[f47,f67])).
% 0.88/0.45 thf(f69,definition,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sF23 @ X8)) = ((X8 @ sK12)))) )),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[sF23])],[function_definition])).
% 0.88/0.45 thf(f70,definition,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sF24 @ X8)) = ((sP0 @ sK11 @ sK14 @ X8)))) )),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[sF24])],[function_definition])).
% 0.88/0.45 thf(f71,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sP0 @ sK11 @ sK14 @ X8)) = ((sF24 @ X8)))) )),
% 0.88/0.45 inference(reorient_equations,[],[f70])).
% 0.88/0.45 thf(f72,definition,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sF25 @ X8)) = ((sK16 @ X8)))) )),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[sF25])],[function_definition])).
% 0.88/0.45 thf(f73,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sK16 @ X8)) = ((sF25 @ X8)))) )),
% 0.88/0.45 inference(reorient_equations,[],[f72])).
% 0.88/0.45 thf(f74,definition,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sF26 @ X8)) = ((sK11 @ sK13 @ (sF25 @ X8))))) )),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[sF26])],[function_definition])).
% 0.88/0.45 thf(f75,definition,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sF27 @ X8)) = ((sK14 @ sK13 @ (sF25 @ X8))))) )),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[sF27])],[function_definition])).
% 0.88/0.45 thf(f76,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sF27 @ X8)) = $true) | (((sF26 @ X8)) = $true) | (((sF23 @ X8)) = $true) | (((sF24 @ X8)) = $true)) )),
% 0.88/0.45 inference(definition_folding,[],[f46,f75,f73,f74,f73,f71,f69])).
% 0.88/0.45 thf(f77,definition,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sF28 @ X8)) = ((X8 @ (sF25 @ X8))))) )),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[sF28])],[function_definition])).
% 0.88/0.45 thf(f78,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((X8 @ (sF25 @ X8))) = ((sF28 @ X8)))) )),
% 0.88/0.45 inference(reorient_equations,[],[f77])).
% 0.88/0.45 thf(f79,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sF24 @ X8)) = $true) | (((sF28 @ X8)) != $true) | (((sF23 @ X8)) = $true)) )),
% 0.88/0.45 inference(definition_folding,[],[f45,f78,f73,f71,f69])).
% 0.88/0.45 thf(f81,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : (($false = ((sF23 @ X8))) | (((X8 @ sK12)) = $true)) )),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f69])).
% 0.88/0.45 thf(f82,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : (($false = ((sF28 @ X8))) | (((X8 @ (sF25 @ X8))) = $true)) )),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f78])).
% 0.88/0.45 thf(f83,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sF28 @ X8)) = $true) | ($false = ((X8 @ (sF25 @ X8))))) )),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f78])).
% 0.88/0.45 thf(f85,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : (($false = ((sF27 @ X8))) | (((sK14 @ sK13 @ (sF25 @ X8))) = $true)) )),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f75])).
% 0.88/0.45 thf(f86,plain,(
% 0.88/0.45 ( ! [X5 : a] : (($false = ((sF18 @ X5))) | (((sK15 @ X5)) = $true)) )),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f57])).
% 0.88/0.45 thf(f87,plain,(
% 0.88/0.45 ( ! [X5 : a] : ((((sF18 @ X5)) = $true) | (((sK15 @ X5)) = $false)) )),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f57])).
% 0.88/0.45 thf(f89,plain,(
% 0.88/0.45 ( ! [X5 : a] : (($true = ((sP3 @ X5 @ sK13 @ sK14))) | ($false = ((sF19 @ X5)))) )),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f59])).
% 0.88/0.45 thf(f91,plain,(
% 0.88/0.45 ( ! [X6 : a,X7 : a] : (($true = ((sP1 @ X7 @ sK11 @ X6))) | ($false = ((sF21 @ X6 @ X7)))) )),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f64])).
% 0.88/0.45 thf(f93,plain,(
% 0.88/0.45 ($false = ((sK15 @ sK12))) | (sF22 = $true)),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f67])).
% 0.88/0.45 thf(f94,plain,(
% 0.88/0.45 ( ! [X6 : a,X7 : a] : ((((sP2 @ X7 @ X6 @ sK14)) = $true) | ($false = ((sF20 @ X6 @ X7)))) )),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f62])).
% 0.88/0.45 thf(f97,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sK11 @ sK13 @ (sF25 @ X8))) = $true) | ($false = ((sF26 @ X8)))) )),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f74])).
% 0.88/0.45 thf(f98,plain,(
% 0.88/0.45 ( ! [X5 : a] : ((((sP4 @ X5 @ sK11 @ sK13)) = $true) | ($false = ((sF17 @ X5)))) )),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f55])).
% 0.88/0.45 thf(f100,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sP0 @ sK11 @ sK14 @ X8)) = $true) | ($false = ((sF24 @ X8)))) )),
% 0.88/0.45 inference(iff_proxy_clausification,[],[f71])).
% 0.88/0.45 thf(f103,definition,(
% 0.88/0.45 spl29_1 <=> (sF22 = $true)),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition])).
% 0.88/0.45 thf(f107,definition,(
% 0.88/0.45 spl29_2 <=> ($false = ((sK15 @ sK12)))),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition])).
% 0.88/0.45 thf(f109,plain,(
% 0.88/0.45 ($false = ((sK15 @ sK12))) | ~spl29_2),
% 0.88/0.45 inference(avatar_component_clause,[],[f107])).
% 0.88/0.45 thf(f110,plain,(
% 0.88/0.45 spl29_1 | spl29_2),
% 0.88/0.45 inference(avatar_split_clause,[],[f93,f107,f103])).
% 0.88/0.45 thf(f120,plain,(
% 0.88/0.45 ~spl29_1),
% 0.88/0.45 inference(avatar_split_clause,[],[f68,f103])).
% 0.88/0.45 thf(f158,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((X8 @ (sK16 @ X8))) = $true) | ($false = ((sF28 @ X8)))) )),
% 0.88/0.45 inference(forward_demodulation,[],[f82,f73])).
% 0.88/0.45 thf(f159,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : (($false = ((X8 @ (sK16 @ X8)))) | (((sF28 @ X8)) = $true)) )),
% 0.88/0.45 inference(forward_demodulation,[],[f83,f73])).
% 0.88/0.45 thf(f161,plain,(
% 0.88/0.45 ($false = $true) | (((sK15 @ (sK16 @ sF18))) = $true) | ($false = ((sF28 @ sF18)))),
% 0.88/0.45 inference(constrained_superposition,[],[f86,f158])).
% 0.88/0.45 thf(f163,plain,(
% 0.88/0.45 (((sK15 @ (sK16 @ sF18))) = $true) | ($false = ((sF28 @ sF18)))),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f161])).
% 0.88/0.45 thf(f165,definition,(
% 0.88/0.45 spl29_5 <=> (((sK15 @ (sK16 @ sF18))) = $true)),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition])).
% 0.88/0.45 thf(f167,plain,(
% 0.88/0.45 (((sK15 @ (sK16 @ sF18))) = $true) | ~spl29_5),
% 0.88/0.45 inference(avatar_component_clause,[],[f165])).
% 0.88/0.45 thf(f169,definition,(
% 0.88/0.45 spl29_6 <=> ($false = ((sF28 @ sF18)))),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[spl29_6])],[avatar_definition])).
% 0.88/0.45 thf(f171,plain,(
% 0.88/0.45 ($false = ((sF28 @ sF18))) | ~spl29_6),
% 0.88/0.45 inference(avatar_component_clause,[],[f169])).
% 0.88/0.45 thf(f173,plain,(
% 0.88/0.45 spl29_5 | spl29_6),
% 0.88/0.45 inference(avatar_split_clause,[],[f163,f169,f165])).
% 0.88/0.45 thf(f177,plain,(
% 0.88/0.45 (((sF28 @ sF18)) = $true) | ($false = $true) | ($false = ((sK15 @ (sK16 @ sF18))))),
% 0.88/0.45 inference(constrained_superposition,[],[f159,f87])).
% 0.88/0.45 thf(f187,plain,(
% 0.88/0.45 (((sF17 @ (sK16 @ sF18))) = $true) | ($false = $true) | (((sF28 @ sF18)) = $true)),
% 0.88/0.45 inference(constrained_superposition,[],[f58,f159])).
% 0.88/0.45 thf(f193,plain,(
% 0.88/0.45 ($false = ((sK15 @ (sK16 @ sF18)))) | (((sF28 @ sF18)) = $true)),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f177])).
% 0.88/0.45 thf(f201,plain,(
% 0.88/0.45 (((sF17 @ (sK16 @ sF18))) = $true) | (((sF28 @ sF18)) = $true)),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f187])).
% 0.88/0.45 thf(f228,plain,(
% 0.88/0.45 ($false = $true) | (((sF17 @ (sK16 @ sF18))) = $true) | ~spl29_6),
% 0.88/0.45 inference(forward_demodulation,[],[f201,f171])).
% 0.88/0.45 thf(f229,plain,(
% 0.88/0.45 (((sF17 @ (sK16 @ sF18))) = $true) | ~spl29_6),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f228])).
% 0.88/0.45 thf(f249,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sK14 @ sK13 @ (sK16 @ X8))) = $true) | ($false = ((sF27 @ X8)))) )),
% 0.88/0.45 inference(forward_demodulation,[],[f85,f73])).
% 0.88/0.45 thf(f251,plain,(
% 0.88/0.45 ( ! [X8 : (a > $o)] : ((((sK11 @ sK13 @ (sK16 @ X8))) = $true) | ($false = ((sF26 @ X8)))) )),
% 0.88/0.45 inference(forward_demodulation,[],[f97,f73])).
% 0.88/0.45 thf(f311,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : a,X1 : (a > a > $o)] : ((((sP4 @ X0 @ X1 @ X2)) != $true) | ($true != $true) | (((X1 @ X2 @ X0)) != $true) | (((sP4 @ X0 @ X1 @ X2)) != $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f30,f32])).
% 0.88/0.45 thf(f313,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : a,X1 : (a > a > $o)] : ((((X1 @ X2 @ X0)) != $true) | ($true != $true) | (((sP4 @ X0 @ X1 @ X2)) != $true)) )),
% 0.88/0.45 inference(duplicate_literal_removal,[],[f311])).
% 0.88/0.45 thf(f314,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : a,X1 : (a > a > $o)] : ((((sP4 @ X0 @ X1 @ X2)) != $true) | (((X1 @ X2 @ X0)) != $true)) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f313])).
% 0.88/0.45 thf(f344,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : a,X1 : (a > a > $o)] : ((((sP1 @ X0 @ X1 @ X2)) != $true) | ($true != $true) | (((X1 @ X2 @ X0)) != $true) | (((sP1 @ X0 @ X1 @ X2)) != $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f40,f41])).
% 0.88/0.45 thf(f348,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : a,X1 : (a > a > $o)] : ((((X1 @ X2 @ X0)) != $true) | ($true != $true) | (((sP1 @ X0 @ X1 @ X2)) != $true)) )),
% 0.88/0.45 inference(duplicate_literal_removal,[],[f344])).
% 0.88/0.45 thf(f349,plain,(
% 0.88/0.45 ( ! [X2 : a,X0 : a,X1 : (a > a > $o)] : ((((sP1 @ X0 @ X1 @ X2)) != $true) | (((X1 @ X2 @ X0)) != $true)) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f348])).
% 0.88/0.45 thf(f353,plain,(
% 0.88/0.45 ( ! [X0 : a] : (($false = ((sF17 @ X0))) | ($true != $true) | (((sK11 @ sK13 @ X0)) != $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f314,f98])).
% 0.88/0.45 thf(f355,plain,(
% 0.88/0.45 ( ! [X0 : a] : ((((sK11 @ sK13 @ X0)) != $true) | ($false = ((sF17 @ X0)))) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f353])).
% 0.88/0.45 thf(f358,plain,(
% 0.88/0.45 ( ! [X0 : (a > $o)] : (($false = ((sF17 @ (sK16 @ X0)))) | ($true != $true) | ($false = ((sF26 @ X0)))) )),
% 0.88/0.45 inference(constrained_superposition,[],[f355,f251])).
% 0.88/0.45 thf(f363,plain,(
% 0.88/0.45 ( ! [X0 : (a > $o)] : (($false = ((sF17 @ (sK16 @ X0)))) | ($false = ((sF26 @ X0)))) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f358])).
% 0.88/0.45 thf(f386,plain,(
% 0.88/0.45 ($false = $true) | ($false = ((sF26 @ sF18))) | ~spl29_6),
% 0.88/0.45 inference(constrained_superposition,[],[f363,f229])).
% 0.88/0.45 thf(f393,plain,(
% 0.88/0.45 ($false = ((sF26 @ sF18))) | ~spl29_6),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f386])).
% 0.88/0.45 thf(f487,plain,(
% 0.88/0.45 ( ! [X2 : (a > a > $o),X0 : a,X1 : a] : ((((sP3 @ X0 @ X1 @ X2)) != $true) | (((X2 @ X1 @ X0)) != $true) | (((sP3 @ X0 @ X1 @ X2)) != $true) | ($true != $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f33,f34])).
% 0.88/0.45 thf(f491,plain,(
% 0.88/0.45 ( ! [X2 : (a > a > $o),X0 : a,X1 : a] : ((((X2 @ X1 @ X0)) != $true) | (((sP3 @ X0 @ X1 @ X2)) != $true) | ($true != $true)) )),
% 0.88/0.45 inference(duplicate_literal_removal,[],[f487])).
% 0.88/0.45 thf(f492,plain,(
% 0.88/0.45 ( ! [X2 : (a > a > $o),X0 : a,X1 : a] : ((((sP3 @ X0 @ X1 @ X2)) != $true) | (((X2 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f491])).
% 0.88/0.45 thf(f495,plain,(
% 0.88/0.45 ( ! [X0 : a,X1 : a] : ((((sK11 @ X1 @ X0)) != $true) | ($false = ((sF21 @ X1 @ X0))) | ($true != $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f349,f91])).
% 0.88/0.45 thf(f503,plain,(
% 0.88/0.45 ( ! [X0 : a,X1 : a] : (($false = ((sF21 @ X1 @ X0))) | (((sK11 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f495])).
% 0.88/0.45 thf(f509,plain,(
% 0.88/0.45 ( ! [X0 : a,X1 : a] : ((((sF18 @ X1)) = $true) | ($false = $true) | (((sK11 @ X0 @ X1)) != $true) | (((sF18 @ X0)) != $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f65,f503])).
% 0.88/0.45 thf(f513,plain,(
% 0.88/0.45 ( ! [X0 : a,X1 : a] : ((((sK11 @ X0 @ X1)) != $true) | (((sF18 @ X0)) != $true) | (((sF18 @ X1)) = $true)) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f509])).
% 0.88/0.45 thf(f526,plain,(
% 0.88/0.45 ( ! [X0 : a,X1 : a] : (($true != $true) | (((sF18 @ X1)) = $true) | (((sF18 @ X0)) != $true) | ($false = ((sK11 @ X0 @ X1)))) )),
% 0.88/0.45 inference(constrained_superposition,[],[f513,f53])).
% 0.88/0.45 thf(f529,plain,(
% 0.88/0.45 ( ! [X0 : a,X1 : a] : (($false = ((sK11 @ X0 @ X1))) | (((sF18 @ X0)) != $true) | (((sF18 @ X1)) = $true)) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f526])).
% 0.88/0.45 thf(f560,plain,(
% 0.88/0.45 ( ! [X2 : (a > a > $o),X0 : a,X1 : a] : ((((sP2 @ X0 @ X1 @ X2)) != $true) | (((sP2 @ X0 @ X1 @ X2)) != $true) | (((X2 @ X1 @ X0)) != $true) | ($true != $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f36,f37])).
% 0.88/0.45 thf(f564,plain,(
% 0.88/0.45 ( ! [X2 : (a > a > $o),X0 : a,X1 : a] : ((((X2 @ X1 @ X0)) != $true) | ($true != $true) | (((sP2 @ X0 @ X1 @ X2)) != $true)) )),
% 0.88/0.45 inference(duplicate_literal_removal,[],[f560])).
% 0.88/0.45 thf(f565,plain,(
% 0.88/0.45 ( ! [X2 : (a > a > $o),X0 : a,X1 : a] : ((((sP2 @ X0 @ X1 @ X2)) != $true) | (((X2 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f564])).
% 0.88/0.45 thf(f694,plain,(
% 0.88/0.45 ( ! [X0 : a] : ((((sK14 @ sK13 @ X0)) != $true) | ($false = ((sF19 @ X0))) | ($true != $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f492,f89])).
% 0.88/0.45 thf(f697,plain,(
% 0.88/0.45 ( ! [X0 : a] : ((((sK14 @ sK13 @ X0)) != $true) | ($false = ((sF19 @ X0)))) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f694])).
% 0.88/0.45 thf(f699,plain,(
% 0.88/0.45 ( ! [X0 : (a > $o)] : (($false = ((sF19 @ (sK16 @ X0)))) | ($false = ((sF27 @ X0))) | ($true != $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f697,f249])).
% 0.88/0.45 thf(f705,plain,(
% 0.88/0.45 ( ! [X0 : (a > $o)] : (($false = ((sF19 @ (sK16 @ X0)))) | ($false = ((sF27 @ X0)))) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f699])).
% 0.88/0.45 thf(f748,plain,(
% 0.88/0.45 ( ! [X0 : (a > $o)] : (($false = $true) | (((sF18 @ (sK16 @ X0))) = $true) | ($false = ((sF27 @ X0)))) )),
% 0.88/0.45 inference(constrained_superposition,[],[f705,f60])).
% 0.88/0.45 thf(f752,plain,(
% 0.88/0.45 ( ! [X0 : (a > $o)] : ((((sF18 @ (sK16 @ X0))) = $true) | ($false = ((sF27 @ X0)))) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f748])).
% 0.88/0.45 thf(f812,plain,(
% 0.88/0.45 ($false = ((sF27 @ sF18))) | (((sF28 @ sF18)) = $true) | ($false = $true)),
% 0.88/0.45 inference(constrained_superposition,[],[f159,f752])).
% 0.88/0.45 thf(f814,plain,(
% 0.88/0.45 (((sF28 @ sF18)) = $true) | ($false = ((sF27 @ sF18)))),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f812])).
% 0.88/0.45 thf(f818,plain,(
% 0.88/0.45 ($false = $true) | ($false = ((sF27 @ sF18))) | ~spl29_6),
% 0.88/0.45 inference(forward_demodulation,[],[f814,f171])).
% 0.88/0.45 thf(f819,plain,(
% 0.88/0.45 ($false = ((sF27 @ sF18))) | ~spl29_6),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f818])).
% 0.88/0.45 thf(f822,plain,(
% 0.88/0.45 (((sF24 @ sF18)) = $true) | ($false = $true) | (((sF23 @ sF18)) = $true) | (((sF26 @ sF18)) = $true) | ~spl29_6),
% 0.88/0.45 inference(constrained_superposition,[],[f819,f76])).
% 0.88/0.45 thf(f826,plain,(
% 0.88/0.45 (((sF24 @ sF18)) = $true) | (((sF26 @ sF18)) = $true) | (((sF23 @ sF18)) = $true) | ~spl29_6),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f822])).
% 0.88/0.45 thf(f830,plain,(
% 0.88/0.45 (((sF23 @ sF18)) = $true) | ($false = $true) | (((sF24 @ sF18)) = $true) | ~spl29_6),
% 0.88/0.45 inference(forward_demodulation,[],[f826,f393])).
% 0.88/0.45 thf(f831,plain,(
% 0.88/0.45 (((sF24 @ sF18)) = $true) | (((sF23 @ sF18)) = $true) | ~spl29_6),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f830])).
% 0.88/0.45 thf(f833,definition,(
% 0.88/0.45 spl29_28 <=> (((sF24 @ sF18)) = $true)),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[spl29_28])],[avatar_definition])).
% 0.88/0.45 thf(f835,plain,(
% 0.88/0.45 (((sF24 @ sF18)) = $true) | ~spl29_28),
% 0.88/0.45 inference(avatar_component_clause,[],[f833])).
% 0.88/0.45 thf(f837,definition,(
% 0.88/0.45 spl29_29 <=> (((sF23 @ sF18)) = $true)),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[spl29_29])],[avatar_definition])).
% 0.88/0.45 thf(f839,plain,(
% 0.88/0.45 (((sF23 @ sF18)) = $true) | ~spl29_29),
% 0.88/0.45 inference(avatar_component_clause,[],[f837])).
% 0.88/0.45 thf(f841,plain,(
% 0.88/0.45 spl29_28 | spl29_29 | ~spl29_6),
% 0.88/0.45 inference(avatar_split_clause,[],[f831,f169,f837,f833])).
% 0.88/0.45 thf(f843,definition,(
% 0.88/0.45 spl29_30 <=> (((sF28 @ sF18)) = $true)),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[spl29_30])],[avatar_definition])).
% 0.88/0.45 thf(f853,definition,(
% 0.88/0.45 spl29_32 <=> ($false = ((sK15 @ (sK16 @ sF18))))),
% 0.88/0.45 introduced(definition,[new_symbols(definition,[spl29_32])],[avatar_definition])).
% 0.88/0.45 thf(f855,plain,(
% 0.88/0.45 ($false = ((sK15 @ (sK16 @ sF18)))) | ~spl29_32),
% 0.88/0.45 inference(avatar_component_clause,[],[f853])).
% 0.88/0.45 thf(f857,plain,(
% 0.88/0.45 spl29_32 | spl29_30),
% 0.88/0.45 inference(avatar_split_clause,[],[f193,f843,f853])).
% 0.88/0.45 thf(f870,plain,(
% 0.88/0.45 ( ! [X0 : a,X1 : a] : ((((sK14 @ X1 @ X0)) != $true) | ($false = ((sF20 @ X1 @ X0))) | ($true != $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f565,f94])).
% 0.88/0.45 thf(f873,plain,(
% 0.88/0.45 ( ! [X0 : a,X1 : a] : (($false = ((sF20 @ X1 @ X0))) | (((sK14 @ X1 @ X0)) != $true)) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f870])).
% 0.88/0.45 thf(f960,plain,(
% 0.88/0.45 ( ! [X0 : a,X1 : a] : (($false = $true) | (((sF18 @ X0)) != $true) | (((sK14 @ X0 @ X1)) != $true) | (((sF18 @ X1)) = $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f63,f873])).
% 0.88/0.45 thf(f969,plain,(
% 0.88/0.45 ( ! [X0 : a,X1 : a] : ((((sK14 @ X0 @ X1)) != $true) | (((sF18 @ X0)) != $true) | (((sF18 @ X1)) = $true)) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f960])).
% 0.88/0.45 thf(f983,plain,(
% 0.88/0.45 ( ! [X0 : (a > a > $o),X1 : (a > $o)] : ((((sF18 @ (sK10 @ X0 @ sK14 @ X1))) != $true) | ($true = ((X0 @ (sK10 @ X0 @ sK14 @ X1) @ (sK9 @ X0 @ sK14 @ X1)))) | ($true != $true) | (((sF18 @ (sK9 @ X0 @ sK14 @ X1))) = $true) | (((sP0 @ X0 @ sK14 @ X1)) != $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f969,f43])).
% 0.88/0.45 thf(f991,plain,(
% 0.88/0.45 ( ! [X0 : (a > a > $o),X1 : (a > $o)] : (($true = ((X0 @ (sK10 @ X0 @ sK14 @ X1) @ (sK9 @ X0 @ sK14 @ X1)))) | (((sP0 @ X0 @ sK14 @ X1)) != $true) | (((sF18 @ (sK9 @ X0 @ sK14 @ X1))) = $true) | (((sF18 @ (sK10 @ X0 @ sK14 @ X1))) != $true)) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f983])).
% 0.88/0.45 thf(f1111,plain,(
% 0.88/0.45 ( ! [X0 : (a > $o)] : ((((sF18 @ (sK10 @ sK11 @ sK14 @ X0))) != $true) | (((sP0 @ sK11 @ sK14 @ X0)) != $true) | (((sF18 @ (sK9 @ sK11 @ sK14 @ X0))) = $true) | (((sF18 @ (sK9 @ sK11 @ sK14 @ X0))) = $true) | ($false = $true) | (((sF18 @ (sK10 @ sK11 @ sK14 @ X0))) != $true)) )),
% 0.88/0.45 inference(constrained_superposition,[],[f529,f991])).
% 0.88/0.45 thf(f1119,plain,(
% 0.88/0.45 ( ! [X0 : (a > $o)] : ((((sP0 @ sK11 @ sK14 @ X0)) != $true) | ($false = $true) | (((sF18 @ (sK10 @ sK11 @ sK14 @ X0))) != $true) | (((sF18 @ (sK9 @ sK11 @ sK14 @ X0))) = $true)) )),
% 0.88/0.45 inference(duplicate_literal_removal,[],[f1111])).
% 0.88/0.45 thf(f1120,plain,(
% 0.88/0.45 ( ! [X0 : (a > $o)] : ((((sF18 @ (sK9 @ sK11 @ sK14 @ X0))) = $true) | (((sF18 @ (sK10 @ sK11 @ sK14 @ X0))) != $true) | (((sP0 @ sK11 @ sK14 @ X0)) != $true)) )),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f1119])).
% 0.88/0.45 thf(f1163,plain,(
% 0.88/0.45 (((sP0 @ sK11 @ sK14 @ sF18)) != $true) | (((sF18 @ (sK10 @ sK11 @ sK14 @ sF18))) != $true) | ($true != $true) | (((sP0 @ sK11 @ sK14 @ sF18)) != $true)),
% 0.88/0.45 inference(constrained_superposition,[],[f42,f1120])).
% 0.88/0.45 thf(f1166,plain,(
% 0.88/0.45 (((sF18 @ (sK10 @ sK11 @ sK14 @ sF18))) != $true) | ($true != $true) | (((sP0 @ sK11 @ sK14 @ sF18)) != $true)),
% 0.88/0.45 inference(duplicate_literal_removal,[],[f1163])).
% 0.88/0.45 thf(f1167,plain,(
% 0.88/0.45 (((sP0 @ sK11 @ sK14 @ sF18)) != $true) | (((sF18 @ (sK10 @ sK11 @ sK14 @ sF18))) != $true)),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f1166])).
% 0.88/0.45 thf(f1169,plain,(
% 0.88/0.45 (((sP0 @ sK11 @ sK14 @ sF18)) != $true)),
% 0.88/0.45 inference(forward_subsumption_resolution,[],[f1167,f44])).
% 0.88/0.45 thf(f1171,plain,(
% 0.88/0.45 (((sF24 @ sF18)) = $false) | ($true != $true)),
% 0.88/0.45 inference(constrained_superposition,[],[f1169,f100])).
% 0.88/0.45 thf(f1174,plain,(
% 0.88/0.45 (((sF24 @ sF18)) = $false)),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f1171])).
% 0.88/0.45 thf(f1177,plain,(
% 0.88/0.45 ($false = $true) | (((sF28 @ sF18)) != $true) | (((sF23 @ sF18)) = $true)),
% 0.88/0.45 inference(constrained_superposition,[],[f79,f1174])).
% 0.88/0.45 thf(f1178,plain,(
% 0.88/0.45 (((sF28 @ sF18)) != $true) | (((sF23 @ sF18)) = $true)),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f1177])).
% 0.88/0.45 thf(f1184,plain,(
% 0.88/0.45 ($true = ((sF18 @ sK12))) | ($false = $true) | ~spl29_29),
% 0.88/0.45 inference(constrained_superposition,[],[f839,f81])).
% 0.88/0.45 thf(f1186,plain,(
% 0.88/0.45 ($true = ((sF18 @ sK12))) | ~spl29_29),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f1184])).
% 0.88/0.45 thf(f1188,plain,(
% 0.88/0.45 (((sK15 @ sK12)) = $true) | ($false = $true) | ~spl29_29),
% 0.88/0.45 inference(constrained_superposition,[],[f1186,f86])).
% 0.88/0.45 thf(f1191,plain,(
% 0.88/0.45 (((sK15 @ sK12)) = $true) | ~spl29_29),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f1188])).
% 0.88/0.45 thf(f1195,plain,(
% 0.88/0.45 ($false = $true) | (~spl29_2 | ~spl29_29)),
% 0.88/0.45 inference(forward_demodulation,[],[f1191,f109])).
% 0.88/0.45 thf(f1196,plain,(
% 0.88/0.45 $false | (~spl29_2 | ~spl29_29)),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f1195])).
% 0.88/0.45 thf(f1197,plain,(
% 0.88/0.45 ~spl29_2 | ~spl29_29),
% 0.88/0.45 inference(avatar_contradiction_clause,[],[f1196])).
% 0.88/0.45 thf(f1199,plain,(
% 0.88/0.45 ~spl29_30 | spl29_29),
% 0.88/0.45 inference(avatar_split_clause,[],[f1178,f837,f843])).
% 0.88/0.45 thf(f1200,plain,(
% 0.88/0.45 ($false = $true) | (~spl29_5 | ~spl29_32)),
% 0.88/0.45 inference(forward_demodulation,[],[f855,f167])).
% 0.88/0.45 thf(f1201,plain,(
% 0.88/0.45 $false | (~spl29_5 | ~spl29_32)),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f1200])).
% 0.88/0.45 thf(f1202,plain,(
% 0.88/0.45 ~spl29_5 | ~spl29_32),
% 0.88/0.45 inference(avatar_contradiction_clause,[],[f1201])).
% 0.88/0.45 thf(f1203,plain,(
% 0.88/0.45 ($false = $true) | ~spl29_28),
% 0.88/0.45 inference(forward_demodulation,[],[f835,f1174])).
% 0.88/0.45 thf(f1204,plain,(
% 0.88/0.45 $false | ~spl29_28),
% 0.88/0.45 inference(trivial_inequality_removal,[],[f1203])).
% 0.88/0.45 thf(f1205,plain,(
% 0.88/0.45 ~spl29_28),
% 0.88/0.45 inference(avatar_contradiction_clause,[],[f1204])).
% 0.88/0.45 cnf(s1, plain, spl29_1 | spl29_2, inference(sat_conversion,[],[f110])).
% 0.88/0.45 cnf(s3, plain, ~spl29_1, inference(sat_conversion,[],[f120])).
% 0.88/0.45 cnf(s7, plain, spl29_5 | spl29_6, inference(sat_conversion,[],[f173])).
% 0.88/0.45 cnf(s28, plain, ~spl29_6 | spl29_28 | spl29_29, inference(sat_conversion,[],[f841])).
% 0.88/0.45 cnf(s32, plain, spl29_30 | spl29_32, inference(sat_conversion,[],[f857])).
% 0.88/0.45 cnf(s42, plain, ~spl29_2 | ~spl29_29, inference(sat_conversion,[],[f1197])).
% 0.88/0.45 cnf(s44, plain, spl29_29 | ~spl29_30, inference(sat_conversion,[],[f1199])).
% 0.88/0.45 cnf(s45, plain, ~spl29_5 | ~spl29_32, inference(sat_conversion,[],[f1202])).
% 0.88/0.45 cnf(s46, plain, ~spl29_28, inference(sat_conversion,[],[f1205])).
% 0.88/0.45 cnf(s47, plain, ~spl29_6 | spl29_29, inference(rat,[],[s28,s46])).
% 0.88/0.45 cnf(s50, plain, spl29_2, inference(rat,[],[s1,s3])).
% 0.88/0.45 cnf(s51, plain, ~spl29_29, inference(rat,[],[s42,s50])).
% 0.88/0.45 cnf(s53, plain, ~spl29_30, inference(rat,[],[s44,s51])).
% 0.88/0.45 cnf(s54, plain, ~spl29_6, inference(rat,[],[s47,s51])).
% 0.88/0.45 cnf(s56, plain, spl29_32, inference(rat,[],[s32,s53])).
% 0.88/0.45 cnf(s58, plain, spl29_5, inference(rat,[],[s7,s54])).
% 0.88/0.45 cnf(s59, plain, $false, inference(rat,[],[s45,s56,s58])).
% 0.88/0.45 thf(f1206,plain,(
% 0.88/0.45 $false),
% 0.88/0.45 inference(avatar_sat_refutation,[],[s59])).
% 0.88/0.45 % SZS output end Proof for theBenchmark
% 0.88/0.45 % (1376173)------------------------------
% 0.88/0.45 % (1376173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.45 % (1376173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.45 % (1376173)CaDiCaL version: 2.1.3
% 0.88/0.45 % (1376173)Termination reason: Refutation
% 0.88/0.45 % (1376173)Time elapsed: 0.105 s
% 0.88/0.45 % (1376173)Peak memory usage: 13 MB
% 0.88/0.45 % (1376173)Instructions burned: 107 (million)
% 0.88/0.45 % (1376162)Success in time 0.151 s
% 0.88/0.45 % Vampire exiting
%------------------------------------------------------------------------------