%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN036^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 : n011.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:41:37 AM UTC 2026
% Result : Theorem 0.18s 0.30s
% Output : Refutation 0.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN036^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n011.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 16:13:16 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running higher-order theorem proving
% 0.07/0.24 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.18/0.30 % (277007)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.18/0.30 % (277014)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2890612910:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.18/0.30 % (277014)Refutation not found, incomplete strategy
% 0.18/0.30 % (277014)------------------------------
% 0.18/0.30 % (277014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.30 % (277014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.30 % (277014)CaDiCaL version: 2.1.3
% 0.18/0.30 % (277014)Termination reason: Refutation not found, incomplete strategy
% 0.18/0.30 % (277014)Time elapsed: 0.002 s
% 0.18/0.30 % (277014)Peak memory usage: 12 MB
% 0.18/0.30 % (277014)Instructions burned: 4 (million)
% 0.18/0.30 % (277014)------------------------------
% 0.18/0.30 % (277014)------------------------------
% 0.18/0.30 % (277018)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.18/0.30 % (277018)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.18/0.30 % (277013)lrs+10_16_si=on:nwc=1.5:random_seed=912741265:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.18/0.30 % (277012)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1053898443:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.18/0.30 % (277016)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3056161096:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.18/0.30 % (277018)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=3269992410:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.18/0.30 % (277015)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=3899648509: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.18/0.30 % (277020)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1548213718:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.18/0.30 % (277020)Instruction limit reached!
% 0.18/0.30 % (277020)------------------------------
% 0.18/0.30 % (277020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.30 % (277020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.30 % (277020)CaDiCaL version: 2.1.3
% 0.18/0.30 % (277020)Termination reason: Instruction limit
% 0.18/0.30 % (277020)Termination phase: Saturation
% 0.18/0.30 % (277020)Time elapsed: 0.001 s
% 0.18/0.30 % (277020)Peak memory usage: 11 MB
% 0.18/0.30 % (277020)Instructions burned: 3 (million)
% 0.18/0.30 % (277012) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-277007-277012"...
% 0.18/0.30 % (277013) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-277007-277013"...
% 0.18/0.30 % (277018) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-277007-277018"...
% 0.18/0.30 % (277015) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-277007-277015"...
% 0.18/0.30 % (277016)Instruction limit reached!
% 0.18/0.30 % (277016)------------------------------
% 0.18/0.30 % (277016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.30 % (277016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.30 % (277017)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=135823007:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.18/0.30 % (277016)CaDiCaL version: 2.1.3
% 0.18/0.30 % (277016)Termination reason: Instruction limit
% 0.18/0.30 % (277016)Termination phase: Saturation
% 0.18/0.30 % (277016)Time elapsed: 0.013 s
% 0.18/0.30 % (277016)Peak memory usage: 12 MB
% 0.18/0.30 % (277016)Instructions burned: 25 (million)
% 0.18/0.30 % (277012)...printing done.
% 0.18/0.30 % (277012)Refutation found. Thanks to Tanya!
% 0.18/0.30 % SZS status Theorem for theBenchmark
% 0.18/0.30 % SZS output start Proof for theBenchmark
% 0.18/0.30 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.18/0.30 thf(func_def_0, type, cQ: ($i > $o)).
% 0.18/0.30 thf(func_def_1, type, cP: ($i > $o)).
% 0.18/0.30 thf(func_def_5, type, sP0: $o).
% 0.18/0.30 thf(func_def_6, type, sK1: ($i > $i)).
% 0.18/0.30 thf(func_def_14, type, sK9: ($i > $i)).
% 0.18/0.30 thf(func_def_20, type, sK15: ($i > $i)).
% 0.18/0.30 thf(func_def_29, type, sK24: ($i > $i)).
% 0.18/0.30 thf(f1,conjecture,(
% 0.18/0.30 (? [X0 : $i] : ! [X1 : $i] : ((cP @ X0) <=> (cP @ X1)) <=> (? [X0 : $i] : (cQ @ X0) <=> ! [X1 : $i] : (cP @ X1))) <=> (? [X0 : $i] : ! [X1 : $i] : ((cQ @ X0) <=> (cQ @ X1)) <=> (? [X0 : $i] : (cP @ X0) <=> ! [X1 : $i] : (cQ @ X1)))),
% 0.18/0.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cX2129)).
% 0.18/0.30 thf(f2,negated_conjecture,(
% 0.18/0.30 ~((? [X0 : $i] : ! [X1 : $i] : ((cP @ X0) <=> (cP @ X1)) <=> (? [X0 : $i] : (cQ @ X0) <=> ! [X1 : $i] : (cP @ X1))) <=> (? [X0 : $i] : ! [X1 : $i] : ((cQ @ X0) <=> (cQ @ X1)) <=> (? [X0 : $i] : (cP @ X0) <=> ! [X1 : $i] : (cQ @ X1))))),
% 0.18/0.30 inference(negated_conjecture,[status(cth)],[f1])).
% 0.18/0.30 thf(f3,plain,(
% 0.18/0.30 ~((? [X0 : $i] : ! [X1 : $i] : ((cP @ X0) <=> (cP @ X1)) <=> (? [X2 : $i] : (cQ @ X2) <=> ! [X3 : $i] : (cP @ X3))) <=> (? [X4 : $i] : ! [X5 : $i] : ((cQ @ X4) <=> (cQ @ X5)) <=> (? [X6 : $i] : (cP @ X6) <=> ! [X7 : $i] : (cQ @ X7))))),
% 0.18/0.30 inference(rectify,[],[f2])).
% 0.18/0.30 thf(f4,plain,(
% 0.18/0.30 ~((? [X4 : $i] : ! [X5 : $i] : (((cQ @ X5)) = ((cQ @ X4))) <=> (? [X6 : $i] : (((cP @ X6)) = $true) <=> ! [X7 : $i] : ($true = ((cQ @ X7))))) <=> ((! [X3 : $i] : ($true = ((cP @ X3))) <=> ? [X2 : $i] : (((cQ @ X2)) = $true)) <=> ? [X0 : $i] : ! [X1 : $i] : (((cP @ X0)) = ((cP @ X1)))))),
% 0.18/0.30 inference(fool_elimination,[],[f3])).
% 0.18/0.30 thf(f5,plain,(
% 0.18/0.30 ((! [X3 : $i] : ($true = ((cP @ X3))) <=> ? [X2 : $i] : (((cQ @ X2)) = $true)) <=> ? [X0 : $i] : ! [X1 : $i] : (((cP @ X0)) = ((cP @ X1)))) <~> (? [X4 : $i] : ! [X5 : $i] : (((cQ @ X5)) = ((cQ @ X4))) <=> (? [X6 : $i] : (((cP @ X6)) = $true) <=> ! [X7 : $i] : ($true = ((cQ @ X7)))))),
% 0.18/0.30 inference(ennf_transformation,[],[f4])).
% 0.18/0.30 thf(f6,definition,(
% 0.18/0.30 ($true = sP0) <=> ((! [X3 : $i] : ($true = ((cP @ X3))) <=> ? [X2 : $i] : (((cQ @ X2)) = $true)) <=> ? [X0 : $i] : ! [X1 : $i] : (((cP @ X0)) = ((cP @ X1))))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 0.18/0.30 thf(f7,plain,(
% 0.18/0.30 ($true = sP0) <~> (? [X4 : $i] : ! [X5 : $i] : (((cQ @ X5)) = ((cQ @ X4))) <=> (? [X6 : $i] : (((cP @ X6)) = $true) <=> ! [X7 : $i] : ($true = ((cQ @ X7)))))),
% 0.18/0.30 inference(definition_folding,[],[f5,f6])).
% 0.18/0.30 thf(f8,plain,(
% 0.18/0.30 (($true = sP0) | ((! [X0 : $i] : ? [X1 : $i] : (((cP @ X0)) != ((cP @ X1))) | ((! [X2 : $i] : (((cQ @ X2)) != $true) | ? [X3 : $i] : ($true != ((cP @ X3)))) & (? [X2 : $i] : (((cQ @ X2)) = $true) | ! [X3 : $i] : ($true = ((cP @ X3)))))) & (? [X0 : $i] : ! [X1 : $i] : (((cP @ X0)) = ((cP @ X1))) | ((! [X3 : $i] : ($true = ((cP @ X3))) | ! [X2 : $i] : (((cQ @ X2)) != $true)) & (? [X2 : $i] : (((cQ @ X2)) = $true) | ? [X3 : $i] : ($true != ((cP @ X3)))))))) & (((((! [X3 : $i] : ($true = ((cP @ X3))) | ! [X2 : $i] : (((cQ @ X2)) != $true)) & (? [X2 : $i] : (((cQ @ X2)) = $true) | ? [X3 : $i] : ($true != ((cP @ X3))))) | ! [X0 : $i] : ? [X1 : $i] : (((cP @ X0)) != ((cP @ X1)))) & (? [X0 : $i] : ! [X1 : $i] : (((cP @ X0)) = ((cP @ X1))) | ((! [X2 : $i] : (((cQ @ X2)) != $true) | ? [X3 : $i] : ($true != ((cP @ X3)))) & (? [X2 : $i] : (((cQ @ X2)) = $true) | ! [X3 : $i] : ($true = ((cP @ X3))))))) | ($true != sP0))),
% 0.18/0.30 inference(nnf_transformation,[],[f6])).
% 0.18/0.30 thf(f9,plain,(
% 0.18/0.30 (($true = sP0) | ((! [X0 : $i] : ? [X1 : $i] : (((cP @ X0)) != ((cP @ X1))) | ((! [X2 : $i] : (((cQ @ X2)) != $true) | ? [X3 : $i] : ($true != ((cP @ X3)))) & (? [X4 : $i] : ($true = ((cQ @ X4))) | ! [X5 : $i] : ($true = ((cP @ X5)))))) & (? [X6 : $i] : ! [X7 : $i] : (((cP @ X6)) = ((cP @ X7))) | ((! [X8 : $i] : ($true = ((cP @ X8))) | ! [X9 : $i] : (((cQ @ X9)) != $true)) & (? [X10 : $i] : ($true = ((cQ @ X10))) | ? [X11 : $i] : ($true != ((cP @ X11)))))))) & (((((! [X12 : $i] : ($true = ((cP @ X12))) | ! [X13 : $i] : (((cQ @ X13)) != $true)) & (? [X14 : $i] : (((cQ @ X14)) = $true) | ? [X15 : $i] : (((cP @ X15)) != $true))) | ! [X16 : $i] : ? [X17 : $i] : (((cP @ X17)) != ((cP @ X16)))) & (? [X18 : $i] : ! [X19 : $i] : (((cP @ X18)) = ((cP @ X19))) | ((! [X20 : $i] : ($true != ((cQ @ X20))) | ? [X21 : $i] : ($true != ((cP @ X21)))) & (? [X22 : $i] : ($true = ((cQ @ X22))) | ! [X23 : $i] : (((cP @ X23)) = $true))))) | ($true != sP0))),
% 0.18/0.30 inference(rectify,[],[f8])).
% 0.18/0.30 thf(f10,plain,(
% 0.18/0.30 (($true = sP0) | ((! [X0 : $i] : (((cP @ X0)) != ((cP @ (sK1 @ X0)))) | ((! [X2 : $i] : (((cQ @ X2)) != $true) | (((cP @ sK2)) != $true)) & (($true = ((cQ @ sK3))) | ! [X5 : $i] : ($true = ((cP @ X5)))))) & (! [X7 : $i] : (((cP @ sK4)) = ((cP @ X7))) | ((! [X8 : $i] : ($true = ((cP @ X8))) | ! [X9 : $i] : (((cQ @ X9)) != $true)) & (($true = ((cQ @ sK5))) | (((cP @ sK6)) != $true)))))) & (((((! [X12 : $i] : ($true = ((cP @ X12))) | ! [X13 : $i] : (((cQ @ X13)) != $true)) & (($true = ((cQ @ sK7))) | ($true != ((cP @ sK8))))) | ! [X16 : $i] : (((cP @ X16)) != ((cP @ (sK9 @ X16))))) & (! [X19 : $i] : (((cP @ sK10)) = ((cP @ X19))) | ((! [X20 : $i] : ($true != ((cQ @ X20))) | (((cP @ sK11)) != $true)) & ((((cQ @ sK12)) = $true) | ! [X23 : $i] : (((cP @ X23)) = $true))))) | ($true != sP0))),
% 0.18/0.30 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,sK2,sK3,sK4,sK5,sK6,sK7,sK8,vAPP,sK10,sK11,sK12]),skolemize(X17,sK9 @ X16),skolemize(X3,sK2),skolemize(X4,sK3),skolemize(X6,sK4),skolemize(X10,sK5),skolemize(X11,sK6),skolemize(X14,sK7),skolemize(X15,sK8),skolemize(X17,sK9 @ X16),skolemize(X18,sK10),skolemize(X21,sK11),skolemize(X22,sK12)],[f9])).
% 0.18/0.30 thf(f11,plain,(
% 0.18/0.30 (((((? [X7 : $i] : ($true != ((cQ @ X7))) | ! [X6 : $i] : (((cP @ X6)) != $true)) & (! [X7 : $i] : ($true = ((cQ @ X7))) | ? [X6 : $i] : (((cP @ X6)) = $true))) | ! [X4 : $i] : ? [X5 : $i] : (((cQ @ X5)) != ((cQ @ X4)))) & (((? [X6 : $i] : (((cP @ X6)) = $true) | ? [X7 : $i] : ($true != ((cQ @ X7)))) & (! [X7 : $i] : ($true = ((cQ @ X7))) | ! [X6 : $i] : (((cP @ X6)) != $true))) | ? [X4 : $i] : ! [X5 : $i] : (((cQ @ X5)) = ((cQ @ X4))))) | ($true != sP0)) & (((? [X4 : $i] : ! [X5 : $i] : (((cQ @ X5)) = ((cQ @ X4))) | ((? [X7 : $i] : ($true != ((cQ @ X7))) | ! [X6 : $i] : (((cP @ X6)) != $true)) & (! [X7 : $i] : ($true = ((cQ @ X7))) | ? [X6 : $i] : (((cP @ X6)) = $true)))) & (((? [X6 : $i] : (((cP @ X6)) = $true) | ? [X7 : $i] : ($true != ((cQ @ X7)))) & (! [X7 : $i] : ($true = ((cQ @ X7))) | ! [X6 : $i] : (((cP @ X6)) != $true))) | ! [X4 : $i] : ? [X5 : $i] : (((cQ @ X5)) != ((cQ @ X4))))) | ($true = sP0))),
% 0.18/0.30 inference(nnf_transformation,[],[f7])).
% 0.18/0.30 thf(f12,plain,(
% 0.18/0.30 (((((? [X0 : $i] : (((cQ @ X0)) != $true) | ! [X1 : $i] : (((cP @ X1)) != $true)) & (! [X2 : $i] : (((cQ @ X2)) = $true) | ? [X3 : $i] : ($true = ((cP @ X3))))) | ! [X4 : $i] : ? [X5 : $i] : (((cQ @ X5)) != ((cQ @ X4)))) & (((? [X6 : $i] : (((cP @ X6)) = $true) | ? [X7 : $i] : ($true != ((cQ @ X7)))) & (! [X8 : $i] : (((cQ @ X8)) = $true) | ! [X9 : $i] : ($true != ((cP @ X9))))) | ? [X10 : $i] : ! [X11 : $i] : (((cQ @ X11)) = ((cQ @ X10))))) | ($true != sP0)) & (((? [X12 : $i] : ! [X13 : $i] : (((cQ @ X13)) = ((cQ @ X12))) | ((? [X14 : $i] : (((cQ @ X14)) != $true) | ! [X15 : $i] : (((cP @ X15)) != $true)) & (! [X16 : $i] : ($true = ((cQ @ X16))) | ? [X17 : $i] : ($true = ((cP @ X17)))))) & (((? [X18 : $i] : (((cP @ X18)) = $true) | ? [X19 : $i] : ($true != ((cQ @ X19)))) & (! [X20 : $i] : ($true = ((cQ @ X20))) | ! [X21 : $i] : ($true != ((cP @ X21))))) | ! [X22 : $i] : ? [X23 : $i] : (((cQ @ X23)) != ((cQ @ X22))))) | ($true = sP0))),
% 0.18/0.30 inference(rectify,[],[f11])).
% 0.18/0.30 thf(f13,plain,(
% 0.18/0.30 (((((($true != ((cQ @ sK13))) | ! [X1 : $i] : (((cP @ X1)) != $true)) & (! [X2 : $i] : (((cQ @ X2)) = $true) | ($true = ((cP @ sK14))))) | ! [X4 : $i] : (((cQ @ X4)) != ((cQ @ (sK15 @ X4))))) & (((($true = ((cP @ sK16))) | (((cQ @ sK17)) != $true)) & (! [X8 : $i] : (((cQ @ X8)) = $true) | ! [X9 : $i] : ($true != ((cP @ X9))))) | ! [X11 : $i] : (((cQ @ sK18)) = ((cQ @ X11))))) | ($true != sP0)) & (((! [X13 : $i] : (((cQ @ X13)) = ((cQ @ sK19))) | ((($true != ((cQ @ sK20))) | ! [X15 : $i] : (((cP @ X15)) != $true)) & (! [X16 : $i] : ($true = ((cQ @ X16))) | ($true = ((cP @ sK21)))))) & (((($true = ((cP @ sK22))) | ($true != ((cQ @ sK23)))) & (! [X20 : $i] : ($true = ((cQ @ X20))) | ! [X21 : $i] : ($true != ((cP @ X21))))) | ! [X22 : $i] : (((cQ @ (sK24 @ X22))) != ((cQ @ X22))))) | ($true = sP0))),
% 0.18/0.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,vAPP,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,vAPP]),skolemize(X0,sK13),skolemize(X3,sK14),skolemize(X17,sK9 @ X16),skolemize(X6,sK16),skolemize(X7,sK17),skolemize(X10,sK18),skolemize(X12,sK19),skolemize(X14,sK20),skolemize(X17,sK21),skolemize(X18,sK22),skolemize(X19,sK23),skolemize(X17,sK9 @ X16)],[f12])).
% 0.18/0.30 thf(f14,plain,(
% 0.18/0.30 ( ! [X19 : $i,X23 : $i] : (($true != sP0) | (((cP @ X23)) = $true) | (((cQ @ sK12)) = $true) | (((cP @ sK10)) = ((cP @ X19)))) )),
% 0.18/0.30 inference(cnf_transformation,[],[f10])).
% 0.18/0.30 thf(f16,plain,(
% 0.18/0.30 ( ! [X16 : $i] : ((((cP @ X16)) != ((cP @ (sK9 @ X16)))) | ($true != sP0) | ($true != ((cP @ sK8))) | ($true = ((cQ @ sK7)))) )),
% 0.18/0.30 inference(cnf_transformation,[],[f10])).
% 0.18/0.30 thf(f17,plain,(
% 0.18/0.30 ( ! [X16 : $i,X12 : $i,X13 : $i] : ((((cP @ X16)) != ((cP @ (sK9 @ X16)))) | ($true != sP0) | ($true = ((cP @ X12))) | (((cQ @ X13)) != $true)) )),
% 0.18/0.30 inference(cnf_transformation,[],[f10])).
% 0.18/0.30 thf(f19,plain,(
% 0.18/0.30 ( ! [X8 : $i,X9 : $i,X7 : $i] : (($true = ((cP @ X8))) | (((cP @ sK4)) = ((cP @ X7))) | (((cQ @ X9)) != $true) | ($true = sP0)) )),
% 0.18/0.30 inference(cnf_transformation,[],[f10])).
% 0.18/0.30 thf(f20,plain,(
% 0.18/0.30 ( ! [X0 : $i,X5 : $i] : (($true = ((cQ @ sK3))) | (((cP @ X0)) != ((cP @ (sK1 @ X0)))) | ($true = ((cP @ X5))) | ($true = sP0)) )),
% 0.18/0.30 inference(cnf_transformation,[],[f10])).
% 0.18/0.30 thf(f21,plain,(
% 0.18/0.30 ( ! [X2 : $i,X0 : $i] : ((((cP @ sK2)) != $true) | (((cQ @ X2)) != $true) | (((cP @ X0)) != ((cP @ (sK1 @ X0)))) | ($true = sP0)) )),
% 0.18/0.30 inference(cnf_transformation,[],[f10])).
% 0.18/0.30 thf(f22,plain,(
% 0.18/0.30 ( ! [X21 : $i,X22 : $i,X20 : $i] : ((((cQ @ (sK24 @ X22))) != ((cQ @ X22))) | ($true = sP0) | ($true != ((cP @ X21))) | ($true = ((cQ @ X20)))) )),
% 0.18/0.30 inference(cnf_transformation,[],[f13])).
% 0.18/0.30 thf(f23,plain,(
% 0.18/0.30 ( ! [X22 : $i] : (($true = ((cP @ sK22))) | ($true != ((cQ @ sK23))) | ($true = sP0) | (((cQ @ (sK24 @ X22))) != ((cQ @ X22)))) )),
% 0.18/0.30 inference(cnf_transformation,[],[f13])).
% 0.18/0.30 thf(f24,plain,(
% 0.18/0.30 ( ! [X16 : $i,X13 : $i] : ((((cQ @ X13)) = ((cQ @ sK19))) | ($true = ((cP @ sK21))) | ($true = ((cQ @ X16))) | ($true = sP0)) )),
% 0.18/0.30 inference(cnf_transformation,[],[f13])).
% 0.18/0.30 thf(f26,plain,(
% 0.18/0.30 ( ! [X11 : $i,X8 : $i,X9 : $i] : ((((cQ @ X8)) = $true) | ($true != sP0) | (((cQ @ sK18)) = ((cQ @ X11))) | ($true != ((cP @ X9)))) )),
% 0.18/0.30 inference(cnf_transformation,[],[f13])).
% 0.18/0.30 thf(f28,plain,(
% 0.18/0.30 ( ! [X2 : $i,X4 : $i] : (($true = ((cP @ sK14))) | (((cQ @ X2)) = $true) | ($true != sP0) | (((cQ @ X4)) != ((cQ @ (sK15 @ X4))))) )),
% 0.18/0.30 inference(cnf_transformation,[],[f13])).
% 0.18/0.30 thf(f29,plain,(
% 0.18/0.30 ( ! [X1 : $i,X4 : $i] : (($true != ((cQ @ sK13))) | ($true != sP0) | (((cQ @ X4)) != ((cQ @ (sK15 @ X4)))) | (((cP @ X1)) != $true)) )),
% 0.18/0.30 inference(cnf_transformation,[],[f13])).
% 0.18/0.30 thf(f37,plain,(
% 0.18/0.30 ( ! [X16 : $i] : (($false = ((cP @ X16))) | ($false = ((cP @ (sK9 @ X16)))) | ($true != sP0) | ($true = ((cQ @ sK7))) | ($true != ((cP @ sK8)))) )),
% 0.18/0.30 inference(xor_proxy_clausification,[],[f16])).
% 0.18/0.30 thf(f38,plain,(
% 0.18/0.30 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true != ((cP @ X9))) | (((cQ @ X11)) = $false) | (((cQ @ X8)) = $true) | ($true = ((cQ @ sK18))) | ($true != sP0)) )),
% 0.18/0.30 inference(iff_proxy_clausification,[],[f26])).
% 0.18/0.30 thf(f39,plain,(
% 0.18/0.30 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true != sP0) | (((cQ @ X8)) = $true) | (((cQ @ sK18)) = $false) | ($true = ((cQ @ X11))) | ($true != ((cP @ X9)))) )),
% 0.18/0.30 inference(iff_proxy_clausification,[],[f26])).
% 0.18/0.30 thf(f40,plain,(
% 0.18/0.30 ( ! [X2 : $i,X4 : $i] : (($true = ((cQ @ X4))) | (((cQ @ X2)) = $true) | ($true = ((cQ @ (sK15 @ X4)))) | ($true = ((cP @ sK14))) | ($true != sP0)) )),
% 0.18/0.30 inference(xor_proxy_clausification,[],[f28])).
% 0.18/0.30 thf(f42,plain,(
% 0.18/0.30 ( ! [X16 : $i,X12 : $i,X13 : $i] : (($true = ((cP @ X12))) | ($true = ((cP @ X16))) | ($true != sP0) | ($true = ((cP @ (sK9 @ X16)))) | (((cQ @ X13)) != $true)) )),
% 0.18/0.30 inference(xor_proxy_clausification,[],[f17])).
% 0.18/0.30 thf(f46,plain,(
% 0.18/0.30 ( ! [X21 : $i,X22 : $i,X20 : $i] : (($true = ((cQ @ X22))) | ($true != ((cP @ X21))) | (((cQ @ (sK24 @ X22))) = $true) | ($true = sP0) | ($true = ((cQ @ X20)))) )),
% 0.18/0.30 inference(xor_proxy_clausification,[],[f22])).
% 0.18/0.30 thf(f48,plain,(
% 0.18/0.30 ( ! [X16 : $i,X13 : $i] : (($true = sP0) | ($true = ((cQ @ X16))) | (((cQ @ sK19)) = $false) | ($true = ((cP @ sK21))) | (((cQ @ X13)) = $true)) )),
% 0.18/0.30 inference(iff_proxy_clausification,[],[f24])).
% 0.18/0.30 thf(f49,plain,(
% 0.18/0.30 ( ! [X16 : $i,X13 : $i] : (($true = ((cP @ sK21))) | (((cQ @ X13)) = $false) | ($true = ((cQ @ X16))) | ($true = sP0) | ($true = ((cQ @ sK19)))) )),
% 0.18/0.30 inference(iff_proxy_clausification,[],[f24])).
% 0.18/0.30 thf(f51,plain,(
% 0.18/0.30 ( ! [X1 : $i,X4 : $i] : (($true != ((cQ @ sK13))) | ($false = ((cQ @ (sK15 @ X4)))) | (((cQ @ X4)) = $false) | (((cP @ X1)) != $true) | ($true != sP0)) )),
% 0.18/0.30 inference(xor_proxy_clausification,[],[f29])).
% 0.18/0.30 thf(f54,plain,(
% 0.18/0.30 ( ! [X19 : $i,X23 : $i] : ((((cQ @ sK12)) = $true) | ($true != sP0) | (((cP @ X19)) = $false) | ($true = ((cP @ sK10))) | (((cP @ X23)) = $true)) )),
% 0.18/0.30 inference(iff_proxy_clausification,[],[f14])).
% 0.18/0.30 thf(f55,plain,(
% 0.18/0.30 ( ! [X19 : $i,X23 : $i] : ((((cP @ sK10)) = $false) | ($true = ((cP @ X19))) | ($true != sP0) | (((cQ @ sK12)) = $true) | (((cP @ X23)) = $true)) )),
% 0.18/0.30 inference(iff_proxy_clausification,[],[f14])).
% 0.18/0.30 thf(f56,plain,(
% 0.18/0.30 ( ! [X8 : $i,X9 : $i,X7 : $i] : (($true = ((cP @ X8))) | ($false = ((cP @ X7))) | ($true = sP0) | ($true = ((cP @ sK4))) | (((cQ @ X9)) != $true)) )),
% 0.18/0.30 inference(iff_proxy_clausification,[],[f19])).
% 0.18/0.30 thf(f57,plain,(
% 0.18/0.30 ( ! [X8 : $i,X9 : $i,X7 : $i] : (($true = ((cP @ X7))) | (((cP @ sK4)) = $false) | (((cQ @ X9)) != $true) | ($true = ((cP @ X8))) | ($true = sP0)) )),
% 0.18/0.30 inference(iff_proxy_clausification,[],[f19])).
% 0.18/0.30 thf(f58,plain,(
% 0.18/0.30 ( ! [X0 : $i,X5 : $i] : ((((cP @ (sK1 @ X0))) = $true) | (((cP @ X0)) = $true) | ($true = ((cQ @ sK3))) | ($true = ((cP @ X5))) | ($true = sP0)) )),
% 0.18/0.30 inference(xor_proxy_clausification,[],[f20])).
% 0.18/0.30 thf(f61,plain,(
% 0.18/0.30 ( ! [X22 : $i] : (($true != ((cQ @ sK23))) | ($true = ((cP @ sK22))) | ($true = sP0) | (((cQ @ (sK24 @ X22))) = $false) | (((cQ @ X22)) = $false)) )),
% 0.18/0.30 inference(xor_proxy_clausification,[],[f23])).
% 0.18/0.30 thf(f63,plain,(
% 0.18/0.30 ( ! [X2 : $i,X0 : $i] : ((((cQ @ X2)) != $true) | (((cP @ sK2)) != $true) | (((cP @ (sK1 @ X0))) = $false) | ($true = sP0) | (((cP @ X0)) = $false)) )),
% 0.18/0.30 inference(xor_proxy_clausification,[],[f21])).
% 0.18/0.30 thf(f69,definition,(
% 0.18/0.30 spl25_2 <=> (((cP @ sK4)) = $false)),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_2])],[avatar_definition])).
% 0.18/0.30 thf(f70,plain,(
% 0.18/0.30 (((cP @ sK4)) != $false) | spl25_2),
% 0.18/0.30 inference(avatar_component_clause,[],[f69])).
% 0.18/0.30 thf(f71,plain,(
% 0.18/0.30 (((cP @ sK4)) = $false) | ~spl25_2),
% 0.18/0.30 inference(avatar_component_clause,[],[f69])).
% 0.18/0.30 thf(f73,definition,(
% 0.18/0.30 spl25_3 <=> ! [X7 : $i] : ($true = ((cP @ X7)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_3])],[avatar_definition])).
% 0.18/0.30 thf(f74,plain,(
% 0.18/0.30 ( ! [X7 : $i] : (($true = ((cP @ X7)))) ) | ~spl25_3),
% 0.18/0.30 inference(avatar_component_clause,[],[f73])).
% 0.18/0.30 thf(f76,definition,(
% 0.18/0.30 spl25_4 <=> ($true = sP0)),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_4])],[avatar_definition])).
% 0.18/0.30 thf(f85,definition,(
% 0.18/0.30 spl25_6 <=> ! [X7 : $i] : ($false = ((cP @ X7)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_6])],[avatar_definition])).
% 0.18/0.30 thf(f86,plain,(
% 0.18/0.30 ( ! [X7 : $i] : (($false = ((cP @ X7)))) ) | ~spl25_6),
% 0.18/0.30 inference(avatar_component_clause,[],[f85])).
% 0.18/0.30 thf(f88,definition,(
% 0.18/0.30 spl25_7 <=> ($true = ((cP @ sK4)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_7])],[avatar_definition])).
% 0.18/0.30 thf(f90,plain,(
% 0.18/0.30 ($true = ((cP @ sK4))) | ~spl25_7),
% 0.18/0.30 inference(avatar_component_clause,[],[f88])).
% 0.18/0.30 thf(f93,definition,(
% 0.18/0.30 spl25_8 <=> ! [X13 : $i] : (((cQ @ X13)) = $false)),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_8])],[avatar_definition])).
% 0.18/0.30 thf(f94,plain,(
% 0.18/0.30 ( ! [X13 : $i] : ((((cQ @ X13)) = $false)) ) | ~spl25_8),
% 0.18/0.30 inference(avatar_component_clause,[],[f93])).
% 0.18/0.30 thf(f96,definition,(
% 0.18/0.30 spl25_9 <=> ($true = ((cQ @ sK19)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_9])],[avatar_definition])).
% 0.18/0.30 thf(f98,plain,(
% 0.18/0.30 ($true = ((cQ @ sK19))) | ~spl25_9),
% 0.18/0.30 inference(avatar_component_clause,[],[f96])).
% 0.18/0.30 thf(f104,definition,(
% 0.18/0.30 spl25_11 <=> ! [X15 : $i] : (((cP @ X15)) != $true)),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_11])],[avatar_definition])).
% 0.18/0.30 thf(f105,plain,(
% 0.18/0.30 ( ! [X15 : $i] : ((((cP @ X15)) != $true)) ) | ~spl25_11),
% 0.18/0.30 inference(avatar_component_clause,[],[f104])).
% 0.18/0.30 thf(f108,definition,(
% 0.18/0.30 spl25_12 <=> ! [X13 : $i] : (((cQ @ X13)) = $true)),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_12])],[avatar_definition])).
% 0.18/0.30 thf(f109,plain,(
% 0.18/0.30 ( ! [X13 : $i] : ((((cQ @ X13)) = $true)) ) | ~spl25_12),
% 0.18/0.30 inference(avatar_component_clause,[],[f108])).
% 0.18/0.30 thf(f111,definition,(
% 0.18/0.30 spl25_13 <=> (((cQ @ sK19)) = $false)),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_13])],[avatar_definition])).
% 0.18/0.30 thf(f113,plain,(
% 0.18/0.30 (((cQ @ sK19)) = $false) | ~spl25_13),
% 0.18/0.30 inference(avatar_component_clause,[],[f111])).
% 0.18/0.30 thf(f116,definition,(
% 0.18/0.30 spl25_14 <=> ($true = ((cP @ sK8)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_14])],[avatar_definition])).
% 0.18/0.30 thf(f118,plain,(
% 0.18/0.30 ($true != ((cP @ sK8))) | spl25_14),
% 0.18/0.30 inference(avatar_component_clause,[],[f116])).
% 0.18/0.30 thf(f120,definition,(
% 0.18/0.30 spl25_15 <=> ! [X16 : $i] : (($false = ((cP @ X16))) | ($false = ((cP @ (sK9 @ X16)))))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_15])],[avatar_definition])).
% 0.18/0.30 thf(f121,plain,(
% 0.18/0.30 ( ! [X16 : $i] : (($false = ((cP @ (sK9 @ X16)))) | ($false = ((cP @ X16)))) ) | ~spl25_15),
% 0.18/0.30 inference(avatar_component_clause,[],[f120])).
% 0.18/0.30 thf(f123,definition,(
% 0.18/0.30 spl25_16 <=> ($true = ((cQ @ sK7)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_16])],[avatar_definition])).
% 0.18/0.30 thf(f125,plain,(
% 0.18/0.30 ($true = ((cQ @ sK7))) | ~spl25_16),
% 0.18/0.30 inference(avatar_component_clause,[],[f123])).
% 0.18/0.30 thf(f126,plain,(
% 0.18/0.30 ~spl25_14 | spl25_15 | spl25_16 | ~spl25_4),
% 0.18/0.30 inference(avatar_split_clause,[],[f37,f76,f123,f120,f116])).
% 0.18/0.30 thf(f128,definition,(
% 0.18/0.30 spl25_17 <=> ! [X16 : $i] : (($true = ((cP @ (sK9 @ X16)))) | ($true = ((cP @ X16))))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_17])],[avatar_definition])).
% 0.18/0.30 thf(f129,plain,(
% 0.18/0.30 ( ! [X16 : $i] : (($true = ((cP @ X16))) | ($true = ((cP @ (sK9 @ X16))))) ) | ~spl25_17),
% 0.18/0.30 inference(avatar_component_clause,[],[f128])).
% 0.18/0.30 thf(f132,definition,(
% 0.18/0.30 spl25_18 <=> (((cQ @ sK18)) = $false)),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_18])],[avatar_definition])).
% 0.18/0.30 thf(f134,plain,(
% 0.18/0.30 (((cQ @ sK18)) = $false) | ~spl25_18),
% 0.18/0.30 inference(avatar_component_clause,[],[f132])).
% 0.18/0.30 thf(f135,plain,(
% 0.18/0.30 spl25_11 | ~spl25_4 | spl25_12 | spl25_12 | spl25_18),
% 0.18/0.30 inference(avatar_split_clause,[],[f39,f132,f108,f108,f76,f104])).
% 0.18/0.30 thf(f137,definition,(
% 0.18/0.30 spl25_19 <=> ($true = ((cQ @ sK18)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_19])],[avatar_definition])).
% 0.18/0.30 thf(f139,plain,(
% 0.18/0.30 ($true = ((cQ @ sK18))) | ~spl25_19),
% 0.18/0.30 inference(avatar_component_clause,[],[f137])).
% 0.18/0.30 thf(f140,plain,(
% 0.18/0.30 spl25_8 | ~spl25_4 | spl25_19 | spl25_12 | spl25_11),
% 0.18/0.30 inference(avatar_split_clause,[],[f38,f104,f108,f137,f76,f93])).
% 0.18/0.30 thf(f142,definition,(
% 0.18/0.30 spl25_20 <=> ($true = ((cP @ sK14)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_20])],[avatar_definition])).
% 0.18/0.30 thf(f144,plain,(
% 0.18/0.30 ($true = ((cP @ sK14))) | ~spl25_20),
% 0.18/0.30 inference(avatar_component_clause,[],[f142])).
% 0.18/0.30 thf(f146,definition,(
% 0.18/0.30 spl25_21 <=> ! [X4 : $i] : ((((cQ @ X4)) = $false) | ($false = ((cQ @ (sK15 @ X4)))))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_21])],[avatar_definition])).
% 0.18/0.30 thf(f147,plain,(
% 0.18/0.30 ( ! [X4 : $i] : (($false = ((cQ @ (sK15 @ X4)))) | (((cQ @ X4)) = $false)) ) | ~spl25_21),
% 0.18/0.30 inference(avatar_component_clause,[],[f146])).
% 0.18/0.30 thf(f150,definition,(
% 0.18/0.30 spl25_22 <=> ! [X4 : $i] : (($true = ((cQ @ X4))) | ($true = ((cQ @ (sK15 @ X4)))))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_22])],[avatar_definition])).
% 0.18/0.30 thf(f151,plain,(
% 0.18/0.30 ( ! [X4 : $i] : (($true = ((cQ @ (sK15 @ X4)))) | ($true = ((cQ @ X4)))) ) | ~spl25_22),
% 0.18/0.30 inference(avatar_component_clause,[],[f150])).
% 0.18/0.30 thf(f152,plain,(
% 0.18/0.30 spl25_22 | ~spl25_4 | spl25_12 | spl25_20),
% 0.18/0.30 inference(avatar_split_clause,[],[f40,f142,f108,f76,f150])).
% 0.18/0.30 thf(f154,definition,(
% 0.18/0.30 spl25_23 <=> ! [X13 : $i] : (((cQ @ X13)) != $true)),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_23])],[avatar_definition])).
% 0.18/0.30 thf(f155,plain,(
% 0.18/0.30 ( ! [X13 : $i] : ((((cQ @ X13)) != $true)) ) | ~spl25_23),
% 0.18/0.30 inference(avatar_component_clause,[],[f154])).
% 0.18/0.30 thf(f157,plain,(
% 0.18/0.30 spl25_3 | spl25_17 | spl25_23 | ~spl25_4),
% 0.18/0.30 inference(avatar_split_clause,[],[f42,f76,f154,f128,f73])).
% 0.18/0.30 thf(f163,definition,(
% 0.18/0.30 spl25_25 <=> (((cP @ sK10)) = $false)),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_25])],[avatar_definition])).
% 0.18/0.30 thf(f165,plain,(
% 0.18/0.30 (((cP @ sK10)) = $false) | ~spl25_25),
% 0.18/0.30 inference(avatar_component_clause,[],[f163])).
% 0.18/0.30 thf(f168,definition,(
% 0.18/0.30 spl25_26 <=> ($true = ((cP @ sK10)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_26])],[avatar_definition])).
% 0.18/0.30 thf(f170,plain,(
% 0.18/0.30 ($true = ((cP @ sK10))) | ~spl25_26),
% 0.18/0.30 inference(avatar_component_clause,[],[f168])).
% 0.18/0.30 thf(f173,definition,(
% 0.18/0.30 spl25_27 <=> ! [X22 : $i] : ((((cQ @ X22)) = $false) | (((cQ @ (sK24 @ X22))) = $false))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_27])],[avatar_definition])).
% 0.18/0.30 thf(f174,plain,(
% 0.18/0.30 ( ! [X22 : $i] : ((((cQ @ (sK24 @ X22))) = $false) | (((cQ @ X22)) = $false)) ) | ~spl25_27),
% 0.18/0.30 inference(avatar_component_clause,[],[f173])).
% 0.18/0.30 thf(f177,definition,(
% 0.18/0.30 spl25_28 <=> ! [X22 : $i] : (($true = ((cQ @ X22))) | (((cQ @ (sK24 @ X22))) = $true))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_28])],[avatar_definition])).
% 0.18/0.30 thf(f178,plain,(
% 0.18/0.30 ( ! [X22 : $i] : ((((cQ @ (sK24 @ X22))) = $true) | ($true = ((cQ @ X22)))) ) | ~spl25_28),
% 0.18/0.30 inference(avatar_component_clause,[],[f177])).
% 0.18/0.30 thf(f179,plain,(
% 0.18/0.30 spl25_11 | spl25_28 | spl25_4 | spl25_12),
% 0.18/0.30 inference(avatar_split_clause,[],[f46,f108,f76,f177,f104])).
% 0.18/0.30 thf(f181,definition,(
% 0.18/0.30 spl25_29 <=> ($true = ((cP @ sK21)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_29])],[avatar_definition])).
% 0.18/0.30 thf(f183,plain,(
% 0.18/0.30 ($true = ((cP @ sK21))) | ~spl25_29),
% 0.18/0.30 inference(avatar_component_clause,[],[f181])).
% 0.18/0.30 thf(f184,plain,(
% 0.18/0.30 spl25_8 | spl25_9 | spl25_4 | spl25_12 | spl25_29),
% 0.18/0.30 inference(avatar_split_clause,[],[f49,f181,f108,f76,f96,f93])).
% 0.18/0.30 thf(f185,plain,(
% 0.18/0.30 spl25_12 | spl25_13 | spl25_29 | spl25_12 | spl25_4),
% 0.18/0.30 inference(avatar_split_clause,[],[f48,f76,f108,f181,f111,f108])).
% 0.18/0.30 thf(f187,definition,(
% 0.18/0.30 spl25_30 <=> ($true = ((cQ @ sK13)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_30])],[avatar_definition])).
% 0.18/0.30 thf(f189,plain,(
% 0.18/0.30 ($true != ((cQ @ sK13))) | spl25_30),
% 0.18/0.30 inference(avatar_component_clause,[],[f187])).
% 0.18/0.30 thf(f190,plain,(
% 0.18/0.30 spl25_11 | ~spl25_4 | ~spl25_30 | spl25_21),
% 0.18/0.30 inference(avatar_split_clause,[],[f51,f146,f187,f76,f104])).
% 0.18/0.30 thf(f203,definition,(
% 0.18/0.30 spl25_33 <=> (((cQ @ sK12)) = $true)),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_33])],[avatar_definition])).
% 0.18/0.30 thf(f205,plain,(
% 0.18/0.30 (((cQ @ sK12)) = $true) | ~spl25_33),
% 0.18/0.30 inference(avatar_component_clause,[],[f203])).
% 0.18/0.30 thf(f206,plain,(
% 0.18/0.30 ~spl25_4 | spl25_25 | spl25_3 | spl25_3 | spl25_33),
% 0.18/0.30 inference(avatar_split_clause,[],[f55,f203,f73,f73,f163,f76])).
% 0.18/0.30 thf(f207,plain,(
% 0.18/0.30 spl25_3 | spl25_26 | spl25_33 | spl25_6 | ~spl25_4),
% 0.18/0.30 inference(avatar_split_clause,[],[f54,f76,f85,f203,f168,f73])).
% 0.18/0.30 thf(f208,plain,(
% 0.18/0.30 spl25_4 | spl25_3 | spl25_3 | spl25_23 | spl25_2),
% 0.18/0.30 inference(avatar_split_clause,[],[f57,f69,f154,f73,f73,f76])).
% 0.18/0.30 thf(f209,plain,(
% 0.18/0.30 spl25_4 | spl25_7 | spl25_3 | spl25_6 | spl25_23),
% 0.18/0.30 inference(avatar_split_clause,[],[f56,f154,f85,f73,f88,f76])).
% 0.18/0.30 thf(f211,definition,(
% 0.18/0.30 spl25_34 <=> ($true = ((cQ @ sK3)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_34])],[avatar_definition])).
% 0.18/0.30 thf(f213,plain,(
% 0.18/0.30 ($true = ((cQ @ sK3))) | ~spl25_34),
% 0.18/0.30 inference(avatar_component_clause,[],[f211])).
% 0.18/0.30 thf(f215,definition,(
% 0.18/0.30 spl25_35 <=> ! [X0 : $i] : ((((cP @ X0)) = $false) | (((cP @ (sK1 @ X0))) = $false))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_35])],[avatar_definition])).
% 0.18/0.30 thf(f216,plain,(
% 0.18/0.30 ( ! [X0 : $i] : ((((cP @ (sK1 @ X0))) = $false) | (((cP @ X0)) = $false)) ) | ~spl25_35),
% 0.18/0.30 inference(avatar_component_clause,[],[f215])).
% 0.18/0.30 thf(f219,definition,(
% 0.18/0.30 spl25_36 <=> ! [X0 : $i] : ((((cP @ (sK1 @ X0))) = $true) | (((cP @ X0)) = $true))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_36])],[avatar_definition])).
% 0.18/0.30 thf(f220,plain,(
% 0.18/0.30 ( ! [X0 : $i] : ((((cP @ X0)) = $true) | (((cP @ (sK1 @ X0))) = $true)) ) | ~spl25_36),
% 0.18/0.30 inference(avatar_component_clause,[],[f219])).
% 0.18/0.30 thf(f221,plain,(
% 0.18/0.30 spl25_3 | spl25_4 | spl25_36 | spl25_34),
% 0.18/0.30 inference(avatar_split_clause,[],[f58,f211,f219,f76,f73])).
% 0.18/0.30 thf(f223,definition,(
% 0.18/0.30 spl25_37 <=> ($true = ((cQ @ sK23)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_37])],[avatar_definition])).
% 0.18/0.30 thf(f225,plain,(
% 0.18/0.30 ($true != ((cQ @ sK23))) | spl25_37),
% 0.18/0.30 inference(avatar_component_clause,[],[f223])).
% 0.18/0.30 thf(f227,definition,(
% 0.18/0.30 spl25_38 <=> ($true = ((cP @ sK22)))),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_38])],[avatar_definition])).
% 0.18/0.30 thf(f229,plain,(
% 0.18/0.30 ($true = ((cP @ sK22))) | ~spl25_38),
% 0.18/0.30 inference(avatar_component_clause,[],[f227])).
% 0.18/0.30 thf(f230,plain,(
% 0.18/0.30 ~spl25_37 | spl25_4 | spl25_27 | spl25_38),
% 0.18/0.30 inference(avatar_split_clause,[],[f61,f227,f173,f76,f223])).
% 0.18/0.30 thf(f233,definition,(
% 0.18/0.30 spl25_39 <=> (((cP @ sK2)) = $true)),
% 0.18/0.30 introduced(definition,[new_symbols(definition,[spl25_39])],[avatar_definition])).
% 0.18/0.30 thf(f235,plain,(
% 0.18/0.30 (((cP @ sK2)) != $true) | spl25_39),
% 0.18/0.30 inference(avatar_component_clause,[],[f233])).
% 0.18/0.30 thf(f236,plain,(
% 0.18/0.30 ~spl25_39 | spl25_23 | spl25_35 | spl25_4),
% 0.18/0.30 inference(avatar_split_clause,[],[f63,f76,f215,f154,f233])).
% 0.18/0.30 thf(f238,plain,(
% 0.18/0.30 $false | (~spl25_12 | spl25_30)),
% 0.18/0.30 inference(forward_subsumption_resolution,[],[f189,f109])).
% 0.18/0.30 thf(f239,plain,(
% 0.18/0.30 ~spl25_12 | spl25_30),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f238])).
% 0.18/0.30 thf(f244,plain,(
% 0.18/0.30 $false | (~spl25_3 | ~spl25_11)),
% 0.18/0.30 inference(forward_subsumption_resolution,[],[f105,f74])).
% 0.18/0.30 thf(f245,plain,(
% 0.18/0.30 ~spl25_3 | ~spl25_11),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f244])).
% 0.18/0.30 thf(f249,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_8 | ~spl25_12)),
% 0.18/0.30 inference(forward_demodulation,[],[f94,f109])).
% 0.18/0.30 thf(f250,plain,(
% 0.18/0.30 $false | (~spl25_8 | ~spl25_12)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f249])).
% 0.18/0.30 thf(f251,plain,(
% 0.18/0.30 ~spl25_8 | ~spl25_12),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f250])).
% 0.18/0.30 thf(f258,plain,(
% 0.18/0.30 $false | (~spl25_12 | ~spl25_23)),
% 0.18/0.30 inference(forward_subsumption_resolution,[],[f155,f109])).
% 0.18/0.30 thf(f259,plain,(
% 0.18/0.30 ~spl25_12 | ~spl25_23),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f258])).
% 0.18/0.30 thf(f268,plain,(
% 0.18/0.30 ( ! [X16 : $i] : (($true = ((cP @ (sK9 @ X16))))) ) | (~spl25_11 | ~spl25_17)),
% 0.18/0.30 inference(forward_subsumption_resolution,[],[f129,f105])).
% 0.18/0.30 thf(f269,plain,(
% 0.18/0.30 $false | (~spl25_11 | ~spl25_17)),
% 0.18/0.30 inference(forward_subsumption_resolution,[],[f268,f105])).
% 0.18/0.30 thf(f270,plain,(
% 0.18/0.30 ~spl25_11 | ~spl25_17),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f269])).
% 0.18/0.30 thf(f271,plain,(
% 0.18/0.30 $false | (~spl25_12 | spl25_37)),
% 0.18/0.30 inference(forward_subsumption_resolution,[],[f225,f109])).
% 0.18/0.30 thf(f272,plain,(
% 0.18/0.30 ~spl25_12 | spl25_37),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f271])).
% 0.18/0.30 thf(f275,plain,(
% 0.18/0.30 ( ! [X0 : $i] : ((((cP @ X0)) = $true)) ) | (~spl25_11 | ~spl25_36)),
% 0.18/0.30 inference(forward_subsumption_resolution,[],[f220,f105])).
% 0.18/0.30 thf(f276,plain,(
% 0.18/0.30 $false | (~spl25_11 | ~spl25_36)),
% 0.18/0.30 inference(forward_subsumption_resolution,[],[f275,f105])).
% 0.18/0.30 thf(f277,plain,(
% 0.18/0.30 ~spl25_11 | ~spl25_36),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f276])).
% 0.18/0.30 thf(f280,plain,(
% 0.18/0.30 ( ! [X22 : $i] : ((((cQ @ (sK24 @ X22))) = $false) | ($true = $false)) ) | (~spl25_12 | ~spl25_27)),
% 0.18/0.30 inference(forward_demodulation,[],[f174,f109])).
% 0.18/0.30 thf(f281,plain,(
% 0.18/0.30 ( ! [X22 : $i] : ((((cQ @ (sK24 @ X22))) = $false)) ) | (~spl25_12 | ~spl25_27)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f280])).
% 0.18/0.30 thf(f282,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_12 | ~spl25_27)),
% 0.18/0.30 inference(forward_demodulation,[],[f281,f109])).
% 0.18/0.30 thf(f283,plain,(
% 0.18/0.30 $false | (~spl25_12 | ~spl25_27)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f282])).
% 0.18/0.30 thf(f284,plain,(
% 0.18/0.30 ~spl25_12 | ~spl25_27),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f283])).
% 0.18/0.30 thf(f291,plain,(
% 0.18/0.30 ( ! [X22 : $i] : ((((cQ @ (sK24 @ X22))) = $true) | ($true = $false)) ) | (~spl25_8 | ~spl25_28)),
% 0.18/0.30 inference(forward_demodulation,[],[f178,f94])).
% 0.18/0.30 thf(f292,plain,(
% 0.18/0.30 ( ! [X22 : $i] : ((((cQ @ (sK24 @ X22))) = $true)) ) | (~spl25_8 | ~spl25_28)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f291])).
% 0.18/0.30 thf(f296,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_8 | ~spl25_33)),
% 0.18/0.30 inference(forward_demodulation,[],[f205,f94])).
% 0.18/0.30 thf(f297,plain,(
% 0.18/0.30 $false | (~spl25_8 | ~spl25_33)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f296])).
% 0.18/0.30 thf(f298,plain,(
% 0.18/0.30 ~spl25_8 | ~spl25_33),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f297])).
% 0.18/0.30 thf(f299,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_8 | ~spl25_28)),
% 0.18/0.30 inference(forward_demodulation,[],[f292,f94])).
% 0.18/0.30 thf(f300,plain,(
% 0.18/0.30 $false | (~spl25_8 | ~spl25_28)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f299])).
% 0.18/0.30 thf(f301,plain,(
% 0.18/0.30 ~spl25_8 | ~spl25_28),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f300])).
% 0.18/0.30 thf(f302,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_9 | ~spl25_13)),
% 0.18/0.30 inference(forward_demodulation,[],[f98,f113])).
% 0.18/0.30 thf(f303,plain,(
% 0.18/0.30 $false | (~spl25_9 | ~spl25_13)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f302])).
% 0.18/0.30 thf(f304,plain,(
% 0.18/0.30 ~spl25_9 | ~spl25_13),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f303])).
% 0.18/0.30 thf(f305,plain,(
% 0.18/0.30 $false | (~spl25_11 | ~spl25_29)),
% 0.18/0.30 inference(forward_subsumption_resolution,[],[f183,f105])).
% 0.18/0.30 thf(f306,plain,(
% 0.18/0.30 ~spl25_11 | ~spl25_29),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f305])).
% 0.18/0.30 thf(f309,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_6 | ~spl25_29)),
% 0.18/0.30 inference(forward_demodulation,[],[f183,f86])).
% 0.18/0.30 thf(f310,plain,(
% 0.18/0.30 $false | (~spl25_6 | ~spl25_29)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f309])).
% 0.18/0.30 thf(f311,plain,(
% 0.18/0.30 ~spl25_6 | ~spl25_29),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f310])).
% 0.18/0.30 thf(f314,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_2 | ~spl25_7)),
% 0.18/0.30 inference(forward_demodulation,[],[f90,f71])).
% 0.18/0.30 thf(f315,plain,(
% 0.18/0.30 $false | (~spl25_2 | ~spl25_7)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f314])).
% 0.18/0.30 thf(f316,plain,(
% 0.18/0.30 ~spl25_2 | ~spl25_7),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f315])).
% 0.18/0.30 thf(f320,plain,(
% 0.18/0.30 ( ! [X0 : $i] : ((((cQ @ X0)) = $true) | ($true != $true)) ) | (~spl25_23 | ~spl25_28)),
% 0.18/0.30 inference(constrained_superposition,[],[f155,f178])).
% 0.18/0.30 thf(f335,plain,(
% 0.18/0.30 ( ! [X0 : $i] : ((((cQ @ X0)) = $true)) ) | (~spl25_23 | ~spl25_28)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f320])).
% 0.18/0.30 thf(f336,plain,(
% 0.18/0.30 $false | (~spl25_23 | ~spl25_28)),
% 0.18/0.30 inference(forward_subsumption_resolution,[],[f335,f155])).
% 0.18/0.30 thf(f337,plain,(
% 0.18/0.30 ~spl25_23 | ~spl25_28),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f336])).
% 0.18/0.30 thf(f342,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_8 | ~spl25_34)),
% 0.18/0.30 inference(constrained_superposition,[],[f213,f94])).
% 0.18/0.30 thf(f344,plain,(
% 0.18/0.30 ($true != $true) | (~spl25_23 | ~spl25_34)),
% 0.18/0.30 inference(constrained_superposition,[],[f155,f213])).
% 0.18/0.30 thf(f347,plain,(
% 0.18/0.30 $false | (~spl25_8 | ~spl25_34)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f342])).
% 0.18/0.30 thf(f348,plain,(
% 0.18/0.30 ~spl25_8 | ~spl25_34),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f347])).
% 0.18/0.30 thf(f349,plain,(
% 0.18/0.30 $false | (~spl25_23 | ~spl25_34)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f344])).
% 0.18/0.30 thf(f350,plain,(
% 0.18/0.30 ~spl25_23 | ~spl25_34),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f349])).
% 0.18/0.30 thf(f357,plain,(
% 0.18/0.30 ($true != $true) | (~spl25_3 | spl25_14)),
% 0.18/0.30 inference(constrained_superposition,[],[f118,f74])).
% 0.18/0.30 thf(f369,plain,(
% 0.18/0.30 $false | (~spl25_3 | spl25_14)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f357])).
% 0.18/0.30 thf(f370,plain,(
% 0.18/0.30 ~spl25_3 | spl25_14),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f369])).
% 0.18/0.30 thf(f381,plain,(
% 0.18/0.30 ($true != $true) | (~spl25_3 | spl25_39)),
% 0.18/0.30 inference(constrained_superposition,[],[f235,f74])).
% 0.18/0.30 thf(f382,plain,(
% 0.18/0.30 $false | (~spl25_3 | spl25_39)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f381])).
% 0.18/0.30 thf(f383,plain,(
% 0.18/0.30 ~spl25_3 | spl25_39),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f382])).
% 0.18/0.30 thf(f385,plain,(
% 0.18/0.30 ( ! [X0 : $i] : (($true = $false) | (((cP @ X0)) = $false)) ) | (~spl25_3 | ~spl25_15)),
% 0.18/0.30 inference(constrained_superposition,[],[f74,f121])).
% 0.18/0.30 thf(f387,plain,(
% 0.18/0.30 ( ! [X0 : $i] : ((((cP @ X0)) = $false)) ) | (~spl25_3 | ~spl25_15)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f385])).
% 0.18/0.30 thf(f391,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_3 | ~spl25_15)),
% 0.18/0.30 inference(forward_demodulation,[],[f387,f74])).
% 0.18/0.30 thf(f392,plain,(
% 0.18/0.30 $false | (~spl25_3 | ~spl25_15)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f391])).
% 0.18/0.30 thf(f393,plain,(
% 0.18/0.30 ~spl25_3 | ~spl25_15),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f392])).
% 0.18/0.30 thf(f395,plain,(
% 0.18/0.30 ( ! [X0 : $i] : (($true = $false) | (((cP @ X0)) = $false)) ) | (~spl25_3 | ~spl25_35)),
% 0.18/0.30 inference(constrained_superposition,[],[f74,f216])).
% 0.18/0.30 thf(f397,plain,(
% 0.18/0.30 ( ! [X0 : $i] : ((((cP @ X0)) = $false)) ) | (~spl25_3 | ~spl25_35)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f395])).
% 0.18/0.30 thf(f401,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_3 | ~spl25_35)),
% 0.18/0.30 inference(forward_demodulation,[],[f397,f74])).
% 0.18/0.30 thf(f402,plain,(
% 0.18/0.30 $false | (~spl25_3 | ~spl25_35)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f401])).
% 0.18/0.30 thf(f403,plain,(
% 0.18/0.30 ~spl25_3 | ~spl25_35),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f402])).
% 0.18/0.30 thf(f426,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_6 | ~spl25_38)),
% 0.18/0.30 inference(constrained_superposition,[],[f229,f86])).
% 0.18/0.30 thf(f427,plain,(
% 0.18/0.30 $false | (~spl25_6 | ~spl25_38)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f426])).
% 0.18/0.30 thf(f428,plain,(
% 0.18/0.30 ~spl25_6 | ~spl25_38),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f427])).
% 0.18/0.30 thf(f435,plain,(
% 0.18/0.30 ( ! [X4 : $i] : (($true = $false) | ($false = ((cQ @ (sK15 @ X4))))) ) | (~spl25_12 | ~spl25_21)),
% 0.18/0.30 inference(forward_demodulation,[],[f147,f109])).
% 0.18/0.30 thf(f436,plain,(
% 0.18/0.30 ( ! [X4 : $i] : (($false = ((cQ @ (sK15 @ X4))))) ) | (~spl25_12 | ~spl25_21)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f435])).
% 0.18/0.30 thf(f437,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_12 | ~spl25_21)),
% 0.18/0.30 inference(forward_demodulation,[],[f436,f109])).
% 0.18/0.30 thf(f438,plain,(
% 0.18/0.30 $false | (~spl25_12 | ~spl25_21)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f437])).
% 0.18/0.30 thf(f439,plain,(
% 0.18/0.30 ~spl25_12 | ~spl25_21),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f438])).
% 0.18/0.30 thf(f440,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_18 | ~spl25_19)),
% 0.18/0.30 inference(forward_demodulation,[],[f134,f139])).
% 0.18/0.30 thf(f441,plain,(
% 0.18/0.30 $false | (~spl25_18 | ~spl25_19)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f440])).
% 0.18/0.30 thf(f442,plain,(
% 0.18/0.30 ~spl25_18 | ~spl25_19),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f441])).
% 0.18/0.30 thf(f448,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_25 | ~spl25_26)),
% 0.18/0.30 inference(forward_demodulation,[],[f165,f170])).
% 0.18/0.30 thf(f449,plain,(
% 0.18/0.30 $false | (~spl25_25 | ~spl25_26)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f448])).
% 0.18/0.30 thf(f450,plain,(
% 0.18/0.30 ~spl25_25 | ~spl25_26),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f449])).
% 0.18/0.30 thf(f451,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_8 | ~spl25_16)),
% 0.18/0.30 inference(forward_demodulation,[],[f125,f94])).
% 0.18/0.30 thf(f452,plain,(
% 0.18/0.30 $false | (~spl25_8 | ~spl25_16)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f451])).
% 0.18/0.30 thf(f453,plain,(
% 0.18/0.30 ~spl25_8 | ~spl25_16),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f452])).
% 0.18/0.30 thf(f484,plain,(
% 0.18/0.30 ( ! [X0 : $i] : (($true = $false) | (((cQ @ X0)) = $true)) ) | (~spl25_8 | ~spl25_22)),
% 0.18/0.30 inference(constrained_superposition,[],[f151,f94])).
% 0.18/0.30 thf(f487,plain,(
% 0.18/0.30 ( ! [X0 : $i] : ((((cQ @ X0)) = $true)) ) | (~spl25_8 | ~spl25_22)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f484])).
% 0.18/0.30 thf(f491,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_8 | ~spl25_22)),
% 0.18/0.30 inference(forward_demodulation,[],[f487,f94])).
% 0.18/0.30 thf(f492,plain,(
% 0.18/0.30 $false | (~spl25_8 | ~spl25_22)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f491])).
% 0.18/0.30 thf(f493,plain,(
% 0.18/0.30 ~spl25_8 | ~spl25_22),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f492])).
% 0.18/0.30 thf(f494,plain,(
% 0.18/0.30 ($true = $false) | (~spl25_6 | ~spl25_20)),
% 0.18/0.30 inference(constrained_superposition,[],[f86,f144])).
% 0.18/0.30 thf(f495,plain,(
% 0.18/0.30 ($false != $false) | (spl25_2 | ~spl25_6)),
% 0.18/0.30 inference(constrained_superposition,[],[f70,f86])).
% 0.18/0.30 thf(f501,plain,(
% 0.18/0.30 $false | (~spl25_6 | ~spl25_20)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f494])).
% 0.18/0.30 thf(f502,plain,(
% 0.18/0.30 ~spl25_6 | ~spl25_20),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f501])).
% 0.18/0.30 thf(f505,plain,(
% 0.18/0.30 $false | (spl25_2 | ~spl25_6)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f495])).
% 0.18/0.30 thf(f506,plain,(
% 0.18/0.30 spl25_2 | ~spl25_6),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f505])).
% 0.18/0.30 thf(f507,plain,(
% 0.18/0.30 ($true != $true) | (~spl25_11 | ~spl25_20)),
% 0.18/0.30 inference(constrained_superposition,[],[f105,f144])).
% 0.18/0.30 thf(f508,plain,(
% 0.18/0.30 $false | (~spl25_11 | ~spl25_20)),
% 0.18/0.30 inference(trivial_inequality_removal,[],[f507])).
% 0.18/0.30 thf(f509,plain,(
% 0.18/0.30 ~spl25_11 | ~spl25_20),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f508])).
% 0.18/0.30 thf(f510,plain,(
% 0.18/0.30 ( ! [X4 : $i] : (($true = ((cQ @ X4)))) ) | (~spl25_22 | ~spl25_23)),
% 0.18/0.30 inference(forward_subsumption_resolution,[],[f151,f155])).
% 0.18/0.30 thf(f511,plain,(
% 0.18/0.30 $false | (~spl25_22 | ~spl25_23)),
% 0.18/0.30 inference(forward_subsumption_resolution,[],[f510,f155])).
% 0.18/0.30 thf(f512,plain,(
% 0.18/0.30 ~spl25_22 | ~spl25_23),
% 0.18/0.30 inference(avatar_contradiction_clause,[],[f511])).
% 0.18/0.30 cnf(s5, plain, ~spl25_4 | ~spl25_14 | spl25_15 | spl25_16, inference(sat_conversion,[],[f126])).
% 0.18/0.30 cnf(s7, plain, spl25_12 | spl25_11 | ~spl25_4 | spl25_12 | spl25_18, inference(sat_conversion,[],[f135])).
% 0.18/0.30 cnf(s8, plain, ~spl25_4 | spl25_11 | spl25_12 | spl25_18, inference(rat,[],[s7])).
% 0.18/0.30 cnf(s9, plain, ~spl25_4 | spl25_8 | spl25_11 | spl25_12 | spl25_19, inference(sat_conversion,[],[f140])).
% 0.18/0.30 cnf(s11, plain, ~spl25_4 | spl25_12 | spl25_20 | spl25_22, inference(sat_conversion,[],[f152])).
% 0.18/0.30 cnf(s13, plain, spl25_3 | ~spl25_4 | spl25_17 | spl25_23, inference(sat_conversion,[],[f157])).
% 0.18/0.30 cnf(s17, plain, spl25_4 | spl25_11 | spl25_12 | spl25_28, inference(sat_conversion,[],[f179])).
% 0.18/0.30 cnf(s18, plain, spl25_4 | spl25_8 | spl25_9 | spl25_12 | spl25_29, inference(sat_conversion,[],[f184])).
% 0.18/0.30 cnf(s19, plain, spl25_12 | spl25_4 | spl25_12 | spl25_13 | spl25_29, inference(sat_conversion,[],[f185])).
% 0.18/0.30 cnf(s20, plain, spl25_4 | spl25_12 | spl25_13 | spl25_29, inference(rat,[],[s19])).
% 0.18/0.30 cnf(s21, plain, ~spl25_4 | spl25_11 | spl25_21 | ~spl25_30, inference(sat_conversion,[],[f190])).
% 0.18/0.30 cnf(s25, plain, spl25_3 | spl25_3 | ~spl25_4 | spl25_25 | spl25_33, inference(sat_conversion,[],[f206])).
% 0.18/0.30 cnf(s26, plain, spl25_3 | ~spl25_4 | spl25_25 | spl25_33, inference(rat,[],[s25])).
% 0.18/0.30 cnf(s27, plain, spl25_3 | ~spl25_4 | spl25_6 | spl25_26 | spl25_33, inference(sat_conversion,[],[f207])).
% 0.18/0.30 cnf(s28, plain, spl25_3 | spl25_2 | spl25_3 | spl25_4 | spl25_23, inference(sat_conversion,[],[f208])).
% 0.18/0.30 cnf(s29, plain, spl25_2 | spl25_3 | spl25_4 | spl25_23, inference(rat,[],[s28])).
% 0.18/0.30 cnf(s30, plain, spl25_3 | spl25_4 | spl25_6 | spl25_7 | spl25_23, inference(sat_conversion,[],[f209])).
% 0.18/0.30 cnf(s32, plain, spl25_3 | spl25_4 | spl25_34 | spl25_36, inference(sat_conversion,[],[f221])).
% 0.18/0.30 cnf(s33, plain, spl25_4 | spl25_27 | ~spl25_37 | spl25_38, inference(sat_conversion,[],[f230])).
% 0.18/0.30 cnf(s35, plain, spl25_4 | spl25_23 | spl25_35 | ~spl25_39, inference(sat_conversion,[],[f236])).
% 0.18/0.30 cnf(s37, plain, ~spl25_12 | spl25_30, inference(sat_conversion,[],[f239])).
% 0.18/0.30 cnf(s40, plain, ~spl25_3 | ~spl25_11, inference(sat_conversion,[],[f245])).
% 0.18/0.30 cnf(s42, plain, ~spl25_8 | ~spl25_12, inference(sat_conversion,[],[f251])).
% 0.18/0.30 cnf(s45, plain, ~spl25_12 | ~spl25_23, inference(sat_conversion,[],[f259])).
% 0.18/0.30 cnf(s47, plain, ~spl25_11 | ~spl25_17, inference(sat_conversion,[],[f270])).
% 0.18/0.30 cnf(s48, plain, ~spl25_12 | spl25_37, inference(sat_conversion,[],[f272])).
% 0.18/0.30 cnf(s50, plain, ~spl25_11 | ~spl25_36, inference(sat_conversion,[],[f277])).
% 0.18/0.30 cnf(s52, plain, ~spl25_12 | ~spl25_27, inference(sat_conversion,[],[f284])).
% 0.18/0.30 cnf(s56, plain, ~spl25_8 | ~spl25_33, inference(sat_conversion,[],[f298])).
% 0.18/0.30 cnf(s57, plain, ~spl25_8 | ~spl25_28, inference(sat_conversion,[],[f301])).
% 0.18/0.30 cnf(s58, plain, ~spl25_9 | ~spl25_13, inference(sat_conversion,[],[f304])).
% 0.18/0.30 cnf(s59, plain, ~spl25_11 | ~spl25_29, inference(sat_conversion,[],[f306])).
% 0.18/0.30 cnf(s60, plain, ~spl25_6 | ~spl25_29, inference(sat_conversion,[],[f311])).
% 0.18/0.30 cnf(s61, plain, ~spl25_2 | ~spl25_7, inference(sat_conversion,[],[f316])).
% 0.18/0.30 cnf(s66, plain, ~spl25_23 | ~spl25_28, inference(sat_conversion,[],[f337])).
% 0.18/0.30 cnf(s68, plain, ~spl25_8 | ~spl25_34, inference(sat_conversion,[],[f348])).
% 0.18/0.30 cnf(s69, plain, ~spl25_23 | ~spl25_34, inference(sat_conversion,[],[f350])).
% 0.18/0.30 cnf(s74, plain, ~spl25_3 | spl25_14, inference(sat_conversion,[],[f370])).
% 0.18/0.30 cnf(s79, plain, ~spl25_3 | spl25_39, inference(sat_conversion,[],[f383])).
% 0.18/0.30 cnf(s81, plain, ~spl25_3 | ~spl25_15, inference(sat_conversion,[],[f393])).
% 0.18/0.30 cnf(s83, plain, ~spl25_3 | ~spl25_35, inference(sat_conversion,[],[f403])).
% 0.18/0.30 cnf(s89, plain, ~spl25_6 | ~spl25_38, inference(sat_conversion,[],[f428])).
% 0.18/0.30 cnf(s93, plain, ~spl25_12 | ~spl25_21, inference(sat_conversion,[],[f439])).
% 0.18/0.30 cnf(s94, plain, ~spl25_18 | ~spl25_19, inference(sat_conversion,[],[f442])).
% 0.18/0.30 cnf(s95, plain, ~spl25_25 | ~spl25_26, inference(sat_conversion,[],[f450])).
% 0.18/0.30 cnf(s96, plain, ~spl25_8 | ~spl25_16, inference(sat_conversion,[],[f453])).
% 0.18/0.30 cnf(s105, plain, ~spl25_8 | ~spl25_22, inference(sat_conversion,[],[f493])).
% 0.18/0.30 cnf(s106, plain, ~spl25_6 | ~spl25_20, inference(sat_conversion,[],[f502])).
% 0.18/0.30 cnf(s108, plain, spl25_2 | ~spl25_6, inference(sat_conversion,[],[f506])).
% 0.18/0.30 cnf(s109, plain, ~spl25_11 | ~spl25_20, inference(sat_conversion,[],[f509])).
% 0.18/0.30 cnf(s110, plain, ~spl25_22 | ~spl25_23, inference(sat_conversion,[],[f512])).
% 0.18/0.30 cnf(s111, plain, spl25_4 | spl25_3 | spl25_2, inference(rat,[],[s50,s17,s32,s45,s66,s69,s29])).
% 0.18/0.30 cnf(s112, plain, ~spl25_11 | ~spl25_4 | spl25_3, inference(rat,[],[s11,s45,s110,s13,s47,s109])).
% 0.18/0.30 cnf(s113, plain, spl25_33 | ~spl25_4 | spl25_3 | spl25_6, inference(rat,[],[s95,s27,s26])).
% 0.18/0.30 cnf(s114, plain, spl25_12 | spl25_8 | spl25_11 | ~spl25_4, inference(rat,[],[s94,s9,s8])).
% 0.18/0.30 cnf(s115, plain, spl25_8 | ~spl25_4 | spl25_11, inference(rat,[],[s21,s37,s93,s114])).
% 0.18/0.30 cnf(s116, plain, spl25_3 | spl25_2, inference(rat,[],[s115,s56,s113,s112,s111,s108])).
% 0.18/0.30 cnf(s117, plain, ~spl25_4 | ~spl25_3, inference(rat,[],[s96,s5,s115,s81,s74,s40])).
% 0.18/0.30 cnf(s118, plain, ~spl25_3, inference(rat,[],[s17,s45,s66,s35,s117,s40,s79,s83])).
% 0.18/0.30 cnf(s119, plain, spl25_2, inference(rat,[],[s116,s118])).
% 0.18/0.30 cnf(s120, plain, ~spl25_7, inference(rat,[],[s61,s119])).
% 0.18/0.30 cnf(s121, plain, ~spl25_4 | spl25_11, inference(rat,[],[s106,s113,s11,s42,s56,s105,s115,s118])).
% 0.18/0.30 cnf(s122, plain, ~spl25_4, inference(rat,[],[s121,s112,s118])).
% 0.18/0.30 cnf(s123, plain, ~spl25_8 | spl25_11, inference(rat,[],[s17,s42,s57,s122])).
% 0.18/0.30 cnf(s124, plain, spl25_12 | spl25_11, inference(rat,[],[s58,s18,s20,s60,s30,s66,s17,s123,s122,s118,s120])).
% 0.18/0.30 cnf(s125, plain, ~spl25_12, inference(rat,[],[s89,s30,s33,s45,s48,s52,s122,s118,s120])).
% 0.18/0.30 cnf(s126, plain, spl25_11, inference(rat,[],[s124,s125])).
% 0.18/0.30 cnf(s128, plain, ~spl25_29, inference(rat,[],[s59,s126])).
% 0.18/0.30 cnf(s130, plain, ~spl25_36, inference(rat,[],[s50,s126])).
% 0.18/0.30 cnf(s132, plain, spl25_13, inference(rat,[],[s20,s125,s122,s128])).
% 0.18/0.30 cnf(s133, plain, spl25_34, inference(rat,[],[s32,s122,s118,s130])).
% 0.18/0.30 cnf(s134, plain, ~spl25_9, inference(rat,[],[s58,s132])).
% 0.18/0.30 cnf(s136, plain, ~spl25_8, inference(rat,[],[s68,s133])).
% 0.18/0.30 cnf(s137, plain, $false, inference(rat,[],[s18,s122,s125,s128,s136,s134])).
% 0.18/0.30 thf(f513,plain,(
% 0.18/0.30 $false),
% 0.18/0.30 inference(avatar_sat_refutation,[],[s137])).
% 0.18/0.30 % SZS output end Proof for theBenchmark
% 0.18/0.30 % (277012)------------------------------
% 0.18/0.30 % (277012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.30 % (277012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.30 % (277012)CaDiCaL version: 2.1.3
% 0.18/0.30 % (277012)Termination reason: Refutation
% 0.18/0.30 % (277012)Time elapsed: 0.014 s
% 0.18/0.30 % (277012)Peak memory usage: 13 MB
% 0.18/0.30 % (277012)Instructions burned: 22 (million)
% 0.18/0.30 % (277007)Success in time 0.05 s
% 0.18/0.30 % Vampire exiting
%------------------------------------------------------------------------------