%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV218^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:38:03 AM UTC 2026
% Result : Theorem 0.22s 0.32s
% Output : Refutation 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV218^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n009.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 15:22:15 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.09/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.32 % (4131219)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.22/0.32 % (4131228)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3526373028:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.22/0.32 % (4131230)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.22/0.32 % (4131230)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.22/0.32 % (4131226)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2901605239:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.22/0.32 % (4131227)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=2847440780: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.22/0.32 % (4131224)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1600797318:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.22/0.32 % (4131225)lrs+10_16_si=on:nwc=1.5:random_seed=1701163199:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.22/0.32 % (4131230)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=460379191:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.22/0.32 % (4131229)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=4266459839:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.22/0.32 % (4131226)Instruction limit reached!
% 0.22/0.32 % (4131226)------------------------------
% 0.22/0.32 % (4131226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.32 % (4131226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.32 % (4131226)CaDiCaL version: 2.1.3
% 0.22/0.32 % (4131226)Termination reason: Instruction limit
% 0.22/0.32 % (4131226)Termination phase: Saturation
% 0.22/0.32 % (4131226)Time elapsed: 0.003 s
% 0.22/0.32 % (4131226)Peak memory usage: 12 MB
% 0.22/0.32 % (4131226)Instructions burned: 4 (million)
% 0.22/0.32 % (4131228)Instruction limit reached!
% 0.22/0.32 % (4131228)------------------------------
% 0.22/0.32 % (4131228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.32 % (4131228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.32 % (4131228)CaDiCaL version: 2.1.3
% 0.22/0.32 % (4131228)Termination reason: Instruction limit
% 0.22/0.32 % (4131228)Termination phase: Saturation
% 0.22/0.32 % (4131228)Time elapsed: 0.008 s
% 0.22/0.32 % (4131228)Peak memory usage: 12 MB
% 0.22/0.32 % (4131228)Instructions burned: 28 (million)
% 0.22/0.32 % (4131225)Instruction limit reached!
% 0.22/0.32 % (4131225)------------------------------
% 0.22/0.32 % (4131225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.32 % (4131225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.32 % (4131225)CaDiCaL version: 2.1.3
% 0.22/0.32 % (4131225)Termination reason: Instruction limit
% 0.22/0.32 % (4131225)Termination phase: Saturation
% 0.22/0.32 % (4131225)Time elapsed: 0.011 s
% 0.22/0.32 % (4131225)Peak memory usage: 12 MB
% 0.22/0.32 % (4131225)Instructions burned: 19 (million)
% 0.22/0.32 % (4131239)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1507108841:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.22/0.32 % (4131239)Instruction limit reached!
% 0.22/0.32 % (4131239)------------------------------
% 0.22/0.32 % (4131239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.32 % (4131239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.32 % (4131239)CaDiCaL version: 2.1.3
% 0.22/0.32 % (4131239)Termination reason: Instruction limit
% 0.22/0.32 % (4131239)Termination phase: Saturation
% 0.22/0.32 % (4131239)Time elapsed: 0.002 s
% 0.22/0.32 % (4131239)Peak memory usage: 12 MB
% 0.22/0.32 % (4131239)Instructions burned: 7 (million)
% 0.22/0.32 % (4131238)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3177229115:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.22/0.32 % (4131238)Instruction limit reached!
% 0.22/0.32 % (4131238)------------------------------
% 0.22/0.32 % (4131238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.32 % (4131238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.32 % (4131238)CaDiCaL version: 2.1.3
% 0.22/0.32 % (4131238)Termination reason: Instruction limit
% 0.22/0.32 % (4131238)Termination phase: Saturation
% 0.22/0.32 % (4131238)Time elapsed: 0.003 s
% 0.22/0.32 % (4131238)Peak memory usage: 12 MB
% 0.22/0.32 % (4131238)Instructions burned: 3 (million)
% 0.22/0.32 % (4131240)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.22/0.32 % (4131230) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4131219-4131230"...
% 0.22/0.32 % (4131242)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1955162410:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.22/0.32 % (4131230)...printing done.
% 0.22/0.32 % (4131240)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3701810702:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.22/0.32 % (4131230)Refutation found. Thanks to Tanya!
% 0.22/0.32 % SZS status Theorem for theBenchmark
% 0.22/0.32 % SZS output start Proof for theBenchmark
% 0.22/0.32 thf(type_def_5, type, a: $tType).
% 0.22/0.32 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.22/0.32 thf(func_def_0, type, cQ: (a > a > $o)).
% 0.22/0.32 thf(func_def_4, type, sP0: $o).
% 0.22/0.32 thf(func_def_5, type, sK1: a).
% 0.22/0.32 thf(func_def_6, type, sK2: a).
% 0.22/0.32 thf(func_def_7, type, sK3: a).
% 0.22/0.32 thf(func_def_8, type, sK4: (a > a > $o)).
% 0.22/0.32 thf(func_def_9, type, sK5: (a > a)).
% 0.22/0.32 thf(func_def_10, type, sK6: a).
% 0.22/0.32 thf(func_def_11, type, sK7: a).
% 0.22/0.32 thf(func_def_12, type, sK8: a).
% 0.22/0.32 thf(func_def_13, type, sF9: (a > $o)).
% 0.22/0.32 thf(func_def_14, type, sF10: (a > a)).
% 0.22/0.32 thf(func_def_15, type, sF11: (a > $o)).
% 0.22/0.32 thf(func_def_16, type, sF12: (a > a > $o)).
% 0.22/0.32 thf(func_def_17, type, sF13: (a > a > $o)).
% 0.22/0.32 thf(func_def_18, type, sF14: $o).
% 0.22/0.32 thf(func_def_19, type, sF15: $o).
% 0.22/0.32 thf(func_def_20, type, sF16: $o).
% 0.22/0.32 thf(f1,conjecture,(
% 0.22/0.32 ? [X0 : (a > a > $o)] : ! [X1 : a] : ((X0 @ X1 @ X1) & ! [X3 : a] : ((X0 @ X1 @ X3) => ! [X4 : a] : ((cQ @ X3 @ X4) <=> (X0 @ X1 @ X4))) & ? [X2 : a] : (X0 @ X1 @ X2)) => (! [X1 : a,X4 : a] : ((cQ @ X1 @ X4) => (cQ @ X4 @ X1)) & ! [X1 : a] : (cQ @ X1 @ X1) & ! [X4 : a,X1 : a,X2 : a] : (((cQ @ X4 @ X2) & (cQ @ X1 @ X4)) => (cQ @ X1 @ X2)))),
% 0.22/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM559A_pme)).
% 0.22/0.32 thf(f2,negated_conjecture,(
% 0.22/0.32 ~(? [X0 : (a > a > $o)] : ! [X1 : a] : ((X0 @ X1 @ X1) & ! [X3 : a] : ((X0 @ X1 @ X3) => ! [X4 : a] : ((cQ @ X3 @ X4) <=> (X0 @ X1 @ X4))) & ? [X2 : a] : (X0 @ X1 @ X2)) => (! [X1 : a,X4 : a] : ((cQ @ X1 @ X4) => (cQ @ X4 @ X1)) & ! [X1 : a] : (cQ @ X1 @ X1) & ! [X4 : a,X1 : a,X2 : a] : (((cQ @ X4 @ X2) & (cQ @ X1 @ X4)) => (cQ @ X1 @ X2))))),
% 0.22/0.32 inference(negated_conjecture,[status(cth)],[f1])).
% 0.22/0.32 thf(f3,plain,(
% 0.22/0.32 ~(? [X0 : (a > a > $o)] : ! [X1 : a] : ((X0 @ X1 @ X1) & ! [X2 : a] : ((X0 @ X1 @ X2) => ! [X3 : a] : ((cQ @ X2 @ X3) <=> (X0 @ X1 @ X3))) & ? [X4 : a] : (X0 @ X1 @ X4)) => (! [X5 : a,X6 : a] : ((cQ @ X5 @ X6) => (cQ @ X6 @ X5)) & ! [X7 : a] : (cQ @ X7 @ X7) & ! [X8 : a,X9 : a,X10 : a] : (((cQ @ X8 @ X10) & (cQ @ X9 @ X8)) => (cQ @ X9 @ X10))))),
% 0.22/0.32 inference(rectify,[],[f2])).
% 0.22/0.32 thf(f4,plain,(
% 0.22/0.32 ~(? [X0 : (a > a > $o)] : ! [X1 : a] : ((((X0 @ X1 @ X1)) = $true) & ? [X4 : a] : (((X0 @ X1 @ X4)) = $true) & ! [X2 : a] : ((((X0 @ X1 @ X2)) = $true) => ! [X3 : a] : (((X0 @ X1 @ X3)) = ((cQ @ X2 @ X3))))) => (! [X6 : a,X5 : a] : ((((cQ @ X5 @ X6)) = $true) => (((cQ @ X6 @ X5)) = $true)) & ! [X7 : a] : (((cQ @ X7 @ X7)) = $true) & ! [X9 : a,X8 : a,X10 : a] : (((((cQ @ X9 @ X8)) = $true) & (((cQ @ X8 @ X10)) = $true)) => (((cQ @ X9 @ X10)) = $true))))),
% 0.22/0.32 inference(fool_elimination,[],[f3])).
% 0.22/0.32 thf(f5,plain,(
% 0.22/0.32 (? [X6 : a,X5 : a] : ((((cQ @ X6 @ X5)) != $true) & (((cQ @ X5 @ X6)) = $true)) | ? [X7 : a] : (((cQ @ X7 @ X7)) != $true) | ? [X9 : a,X8 : a,X10 : a] : ((((cQ @ X9 @ X10)) != $true) & ((((cQ @ X9 @ X8)) = $true) & (((cQ @ X8 @ X10)) = $true)))) & ? [X0 : (a > a > $o)] : ! [X1 : a] : ((((X0 @ X1 @ X1)) = $true) & ? [X4 : a] : (((X0 @ X1 @ X4)) = $true) & ! [X2 : a] : ((((X0 @ X1 @ X2)) != $true) | ! [X3 : a] : (((X0 @ X1 @ X3)) = ((cQ @ X2 @ X3)))))),
% 0.22/0.32 inference(ennf_transformation,[],[f4])).
% 0.22/0.32 thf(f6,plain,(
% 0.22/0.32 ? [X0 : (a > a > $o)] : ! [X1 : a] : ((((X0 @ X1 @ X1)) = $true) & ? [X4 : a] : (((X0 @ X1 @ X4)) = $true) & ! [X2 : a] : ((((X0 @ X1 @ X2)) != $true) | ! [X3 : a] : (((X0 @ X1 @ X3)) = ((cQ @ X2 @ X3))))) & (? [X7 : a] : (((cQ @ X7 @ X7)) != $true) | ? [X10 : a,X8 : a,X9 : a] : ((((cQ @ X9 @ X8)) = $true) & (((cQ @ X9 @ X10)) != $true) & (((cQ @ X8 @ X10)) = $true)) | ? [X6 : a,X5 : a] : ((((cQ @ X6 @ X5)) != $true) & (((cQ @ X5 @ X6)) = $true)))),
% 0.22/0.32 inference(flattening,[],[f5])).
% 0.22/0.32 thf(f7,definition,(
% 0.22/0.32 ? [X10 : a,X8 : a,X9 : a] : ((((cQ @ X9 @ X8)) = $true) & (((cQ @ X9 @ X10)) != $true) & (((cQ @ X8 @ X10)) = $true)) | ~ ($true = sP0)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 0.22/0.32 thf(f8,plain,(
% 0.22/0.32 ? [X0 : (a > a > $o)] : ! [X1 : a] : ((((X0 @ X1 @ X1)) = $true) & ? [X4 : a] : (((X0 @ X1 @ X4)) = $true) & ! [X2 : a] : ((((X0 @ X1 @ X2)) != $true) | ! [X3 : a] : (((X0 @ X1 @ X3)) = ((cQ @ X2 @ X3))))) & (? [X7 : a] : (((cQ @ X7 @ X7)) != $true) | ($true = sP0) | ? [X6 : a,X5 : a] : ((((cQ @ X6 @ X5)) != $true) & (((cQ @ X5 @ X6)) = $true)))),
% 0.22/0.32 inference(definition_folding,[],[f6,f7])).
% 0.22/0.32 thf(f9,plain,(
% 0.22/0.32 ? [X10 : a,X8 : a,X9 : a] : ((((cQ @ X9 @ X8)) = $true) & (((cQ @ X9 @ X10)) != $true) & (((cQ @ X8 @ X10)) = $true)) | ($true != sP0)),
% 0.22/0.32 inference(nnf_transformation,[],[f7])).
% 0.22/0.32 thf(f10,plain,(
% 0.22/0.32 ? [X0 : a,X1 : a,X2 : a] : ((((cQ @ X2 @ X1)) = $true) & (((cQ @ X2 @ X0)) != $true) & (((cQ @ X1 @ X0)) = $true)) | ($true != sP0)),
% 0.22/0.32 inference(rectify,[],[f9])).
% 0.22/0.32 thf(f11,plain,(
% 0.22/0.32 ((((cQ @ sK3 @ sK2)) = $true) & (((cQ @ sK3 @ sK1)) != $true) & (((cQ @ sK2 @ sK1)) = $true)) | ($true != sP0)),
% 0.22/0.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3)],[f10])).
% 0.22/0.32 thf(f12,plain,(
% 0.22/0.32 ? [X0 : (a > a > $o)] : ! [X1 : a] : ((((X0 @ X1 @ X1)) = $true) & ? [X2 : a] : (((X0 @ X1 @ X2)) = $true) & ! [X3 : a] : ((((X0 @ X1 @ X3)) != $true) | ! [X4 : a] : (((X0 @ X1 @ X4)) = ((cQ @ X3 @ X4))))) & (? [X5 : a] : (((cQ @ X5 @ X5)) != $true) | ($true = sP0) | ? [X6 : a,X7 : a] : (($true != ((cQ @ X6 @ X7))) & (((cQ @ X7 @ X6)) = $true)))),
% 0.22/0.32 inference(rectify,[],[f8])).
% 0.22/0.32 thf(f13,plain,(
% 0.22/0.32 ! [X1 : a] : (($true = ((sK4 @ X1 @ X1))) & (((sK4 @ X1 @ (sK5 @ X1))) = $true) & ! [X3 : a] : ((((sK4 @ X1 @ X3)) != $true) | ! [X4 : a] : (((cQ @ X3 @ X4)) = ((sK4 @ X1 @ X4))))) & ((((cQ @ sK6 @ sK6)) != $true) | ($true = sP0) | ((((cQ @ sK7 @ sK8)) != $true) & ($true = ((cQ @ sK8 @ sK7)))))),
% 0.22/0.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK4,vAPP,sK6,sK7,sK8]),skolemize(X0,sK4),skolemize(X2,sK5 @ X1),skolemize(X5,sK6),skolemize(X6,sK7),skolemize(X7,sK8)],[f12])).
% 0.22/0.32 thf(f14,plain,(
% 0.22/0.32 ($true != sP0) | (((cQ @ sK2 @ sK1)) = $true)),
% 0.22/0.32 inference(cnf_transformation,[],[f11])).
% 0.22/0.32 thf(f15,plain,(
% 0.22/0.32 (((cQ @ sK3 @ sK1)) != $true) | ($true != sP0)),
% 0.22/0.32 inference(cnf_transformation,[],[f11])).
% 0.22/0.32 thf(f16,plain,(
% 0.22/0.32 (((cQ @ sK3 @ sK2)) = $true) | ($true != sP0)),
% 0.22/0.32 inference(cnf_transformation,[],[f11])).
% 0.22/0.32 thf(f17,plain,(
% 0.22/0.32 (((cQ @ sK6 @ sK6)) != $true) | ($true = sP0) | ($true = ((cQ @ sK8 @ sK7)))),
% 0.22/0.32 inference(cnf_transformation,[],[f13])).
% 0.22/0.32 thf(f18,plain,(
% 0.22/0.32 (((cQ @ sK6 @ sK6)) != $true) | ($true = sP0) | (((cQ @ sK7 @ sK8)) != $true)),
% 0.22/0.32 inference(cnf_transformation,[],[f13])).
% 0.22/0.32 thf(f19,plain,(
% 0.22/0.32 ( ! [X3 : a,X1 : a,X4 : a] : ((((sK4 @ X1 @ X3)) != $true) | (((cQ @ X3 @ X4)) = ((sK4 @ X1 @ X4)))) )),
% 0.22/0.32 inference(cnf_transformation,[],[f13])).
% 0.22/0.32 thf(f21,plain,(
% 0.22/0.32 ( ! [X1 : a] : (($true = ((sK4 @ X1 @ X1)))) )),
% 0.22/0.32 inference(cnf_transformation,[],[f13])).
% 0.22/0.32 thf(f23,definition,(
% 0.22/0.32 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.22/0.32 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.22/0.32 thf(f24,definition,(
% 0.22/0.32 ( ! [X1 : a] : ((((sF9 @ X1)) = ((sK4 @ X1 @ X1)))) )),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 0.22/0.32 thf(f25,plain,(
% 0.22/0.32 ( ! [X1 : a] : (($true = ((sF9 @ X1)))) )),
% 0.22/0.32 inference(definition_folding,[],[f21,f24])).
% 0.22/0.32 thf(f29,definition,(
% 0.22/0.32 ( ! [X3 : a,X1 : a] : ((((sF12 @ X3 @ X1)) = ((sK4 @ X1 @ X3)))) )),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 0.22/0.32 thf(f30,plain,(
% 0.22/0.32 ( ! [X3 : a,X1 : a] : ((((sK4 @ X1 @ X3)) = ((sF12 @ X3 @ X1)))) )),
% 0.22/0.32 inference(reorient_equations,[],[f29])).
% 0.22/0.32 thf(f31,definition,(
% 0.22/0.32 ( ! [X3 : a,X4 : a] : ((((sF13 @ X4 @ X3)) = ((cQ @ X3 @ X4)))) )),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 0.22/0.32 thf(f32,plain,(
% 0.22/0.32 ( ! [X3 : a,X4 : a] : ((((cQ @ X3 @ X4)) = ((sF13 @ X4 @ X3)))) )),
% 0.22/0.32 inference(reorient_equations,[],[f31])).
% 0.22/0.32 thf(f33,plain,(
% 0.22/0.32 ( ! [X3 : a,X1 : a,X4 : a] : ((((sF12 @ X3 @ X1)) != $true) | (((sF13 @ X4 @ X3)) = ((sF12 @ X4 @ X1)))) )),
% 0.22/0.32 inference(definition_folding,[],[f19,f30,f32,f30])).
% 0.22/0.32 thf(f34,definition,(
% 0.22/0.32 (sF14 = ((cQ @ sK6 @ sK6)))),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 0.22/0.32 thf(f35,definition,(
% 0.22/0.32 (sF15 = ((cQ @ sK7 @ sK8)))),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 0.22/0.32 thf(f36,plain,(
% 0.22/0.32 (sF14 != $true) | (sF15 != $true) | ($true = sP0)),
% 0.22/0.32 inference(definition_folding,[],[f18,f35,f34])).
% 0.22/0.32 thf(f37,definition,(
% 0.22/0.32 (sF16 = ((cQ @ sK8 @ sK7)))),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 0.22/0.32 thf(f38,plain,(
% 0.22/0.32 (sF16 = $true) | ($true = sP0) | (sF14 != $true)),
% 0.22/0.32 inference(definition_folding,[],[f17,f37,f34])).
% 0.22/0.32 thf(f39,plain,(
% 0.22/0.32 ($false = ((cQ @ sK7 @ sK8))) | (sF15 = $true)),
% 0.22/0.32 inference(iff_proxy_clausification,[],[f35])).
% 0.22/0.32 thf(f44,plain,(
% 0.22/0.32 (sF16 = $false) | ($true = ((cQ @ sK8 @ sK7)))),
% 0.22/0.32 inference(iff_proxy_clausification,[],[f37])).
% 0.22/0.32 thf(f45,plain,(
% 0.22/0.32 (sF14 = $true) | ($false = ((cQ @ sK6 @ sK6)))),
% 0.22/0.32 inference(iff_proxy_clausification,[],[f34])).
% 0.22/0.32 thf(f47,plain,(
% 0.22/0.32 ( ! [X3 : a,X1 : a,X4 : a] : (($false = ((sF12 @ X4 @ X1))) | (((sF12 @ X3 @ X1)) != $true) | (((sF13 @ X4 @ X3)) = $true)) )),
% 0.22/0.32 inference(iff_proxy_clausification,[],[f33])).
% 0.22/0.32 thf(f48,plain,(
% 0.22/0.32 ( ! [X3 : a,X1 : a,X4 : a] : ((((sF13 @ X4 @ X3)) = $false) | (((sF12 @ X4 @ X1)) = $true) | (((sF12 @ X3 @ X1)) != $true)) )),
% 0.22/0.32 inference(iff_proxy_clausification,[],[f33])).
% 0.22/0.32 thf(f50,plain,(
% 0.22/0.32 ( ! [X3 : a,X1 : a] : (($false = ((sK4 @ X1 @ X3))) | (((sF12 @ X3 @ X1)) = $true)) )),
% 0.22/0.32 inference(iff_proxy_clausification,[],[f30])).
% 0.22/0.32 thf(f52,plain,(
% 0.22/0.32 ( ! [X1 : a] : (($false = ((sF9 @ X1))) | ($true = ((sK4 @ X1 @ X1)))) )),
% 0.22/0.32 inference(iff_proxy_clausification,[],[f24])).
% 0.22/0.32 thf(f53,plain,(
% 0.22/0.32 ( ! [X3 : a,X4 : a] : ((((sF13 @ X4 @ X3)) = $false) | (((cQ @ X3 @ X4)) = $true)) )),
% 0.22/0.32 inference(iff_proxy_clausification,[],[f32])).
% 0.22/0.32 thf(f54,plain,(
% 0.22/0.32 ( ! [X3 : a,X4 : a] : ((((sF13 @ X4 @ X3)) = $true) | (((cQ @ X3 @ X4)) = $false)) )),
% 0.22/0.32 inference(iff_proxy_clausification,[],[f32])).
% 0.22/0.32 thf(f65,definition,(
% 0.22/0.32 spl17_3 <=> ($false = ((cQ @ sK7 @ sK8)))),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_3])],[avatar_definition])).
% 0.22/0.32 thf(f67,plain,(
% 0.22/0.32 ($false = ((cQ @ sK7 @ sK8))) | ~spl17_3),
% 0.22/0.32 inference(avatar_component_clause,[],[f65])).
% 0.22/0.32 thf(f69,definition,(
% 0.22/0.32 spl17_4 <=> (sF15 = $true)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_4])],[avatar_definition])).
% 0.22/0.32 thf(f72,plain,(
% 0.22/0.32 spl17_3 | spl17_4),
% 0.22/0.32 inference(avatar_split_clause,[],[f39,f69,f65])).
% 0.22/0.32 thf(f74,definition,(
% 0.22/0.32 spl17_5 <=> (sF16 = $false)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_5])],[avatar_definition])).
% 0.22/0.32 thf(f76,plain,(
% 0.22/0.32 (sF16 = $false) | ~spl17_5),
% 0.22/0.32 inference(avatar_component_clause,[],[f74])).
% 0.22/0.32 thf(f78,definition,(
% 0.22/0.32 spl17_6 <=> ($true = ((cQ @ sK8 @ sK7)))),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_6])],[avatar_definition])).
% 0.22/0.32 thf(f80,plain,(
% 0.22/0.32 ($true = ((cQ @ sK8 @ sK7))) | ~spl17_6),
% 0.22/0.32 inference(avatar_component_clause,[],[f78])).
% 0.22/0.32 thf(f81,plain,(
% 0.22/0.32 spl17_5 | spl17_6),
% 0.22/0.32 inference(avatar_split_clause,[],[f44,f78,f74])).
% 0.22/0.32 thf(f83,definition,(
% 0.22/0.32 spl17_7 <=> (sF16 = $true)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_7])],[avatar_definition])).
% 0.22/0.32 thf(f85,plain,(
% 0.22/0.32 (sF16 = $true) | ~spl17_7),
% 0.22/0.32 inference(avatar_component_clause,[],[f83])).
% 0.22/0.32 thf(f92,definition,(
% 0.22/0.32 spl17_9 <=> (((cQ @ sK6 @ sK6)) = $true)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_9])],[avatar_definition])).
% 0.22/0.32 thf(f93,plain,(
% 0.22/0.32 (((cQ @ sK6 @ sK6)) != $true) | spl17_9),
% 0.22/0.32 inference(avatar_component_clause,[],[f92])).
% 0.22/0.32 thf(f94,plain,(
% 0.22/0.32 (((cQ @ sK6 @ sK6)) = $true) | ~spl17_9),
% 0.22/0.32 inference(avatar_component_clause,[],[f92])).
% 0.22/0.32 thf(f101,definition,(
% 0.22/0.32 spl17_11 <=> (sF14 = $true)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_11])],[avatar_definition])).
% 0.22/0.32 thf(f105,definition,(
% 0.22/0.32 spl17_12 <=> ($false = ((cQ @ sK6 @ sK6)))),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_12])],[avatar_definition])).
% 0.22/0.32 thf(f107,plain,(
% 0.22/0.32 ($false = ((cQ @ sK6 @ sK6))) | ~spl17_12),
% 0.22/0.32 inference(avatar_component_clause,[],[f105])).
% 0.22/0.32 thf(f108,plain,(
% 0.22/0.32 spl17_11 | spl17_12),
% 0.22/0.32 inference(avatar_split_clause,[],[f45,f105,f101])).
% 0.22/0.32 thf(f110,definition,(
% 0.22/0.32 spl17_13 <=> ($true = sP0)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_13])],[avatar_definition])).
% 0.22/0.32 thf(f114,definition,(
% 0.22/0.32 spl17_14 <=> (((cQ @ sK2 @ sK1)) = $true)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_14])],[avatar_definition])).
% 0.22/0.32 thf(f116,plain,(
% 0.22/0.32 (((cQ @ sK2 @ sK1)) = $true) | ~spl17_14),
% 0.22/0.32 inference(avatar_component_clause,[],[f114])).
% 0.22/0.32 thf(f117,plain,(
% 0.22/0.32 ~spl17_13 | spl17_14),
% 0.22/0.32 inference(avatar_split_clause,[],[f14,f114,f110])).
% 0.22/0.32 thf(f119,definition,(
% 0.22/0.32 spl17_15 <=> (((cQ @ sK3 @ sK1)) = $true)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_15])],[avatar_definition])).
% 0.22/0.32 thf(f121,plain,(
% 0.22/0.32 (((cQ @ sK3 @ sK1)) != $true) | spl17_15),
% 0.22/0.32 inference(avatar_component_clause,[],[f119])).
% 0.22/0.32 thf(f122,plain,(
% 0.22/0.32 ~spl17_13 | ~spl17_15),
% 0.22/0.32 inference(avatar_split_clause,[],[f15,f119,f110])).
% 0.22/0.32 thf(f123,plain,(
% 0.22/0.32 ~spl17_11 | spl17_7 | spl17_13),
% 0.22/0.32 inference(avatar_split_clause,[],[f38,f110,f83,f101])).
% 0.22/0.32 thf(f125,definition,(
% 0.22/0.32 spl17_16 <=> (((cQ @ sK3 @ sK2)) = $true)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_16])],[avatar_definition])).
% 0.22/0.32 thf(f127,plain,(
% 0.22/0.32 (((cQ @ sK3 @ sK2)) = $true) | ~spl17_16),
% 0.22/0.32 inference(avatar_component_clause,[],[f125])).
% 0.22/0.32 thf(f128,plain,(
% 0.22/0.32 ~spl17_13 | spl17_16),
% 0.22/0.32 inference(avatar_split_clause,[],[f16,f125,f110])).
% 0.22/0.32 thf(f129,plain,(
% 0.22/0.32 spl17_13 | ~spl17_11 | ~spl17_4),
% 0.22/0.32 inference(avatar_split_clause,[],[f36,f69,f101,f110])).
% 0.22/0.32 thf(f130,plain,(
% 0.22/0.32 ($false = $true) | (~spl17_5 | ~spl17_7)),
% 0.22/0.32 inference(forward_demodulation,[],[f85,f76])).
% 0.22/0.32 thf(f131,plain,(
% 0.22/0.32 $false | (~spl17_5 | ~spl17_7)),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f130])).
% 0.22/0.32 thf(f132,plain,(
% 0.22/0.32 ~spl17_5 | ~spl17_7),
% 0.22/0.32 inference(avatar_contradiction_clause,[],[f131])).
% 0.22/0.32 thf(f167,plain,(
% 0.22/0.32 ($false = $true) | (~spl17_9 | ~spl17_12)),
% 0.22/0.32 inference(forward_demodulation,[],[f107,f94])).
% 0.22/0.32 thf(f168,plain,(
% 0.22/0.32 $false | (~spl17_9 | ~spl17_12)),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f167])).
% 0.22/0.32 thf(f169,plain,(
% 0.22/0.32 ~spl17_9 | ~spl17_12),
% 0.22/0.32 inference(avatar_contradiction_clause,[],[f168])).
% 0.22/0.32 thf(f191,plain,(
% 0.22/0.32 ( ! [X1 : a] : (($true = ((sK4 @ X1 @ X1))) | ($false = $true)) )),
% 0.22/0.32 inference(forward_demodulation,[],[f52,f25])).
% 0.22/0.32 thf(f192,plain,(
% 0.22/0.32 ( ! [X1 : a] : (($true = ((sK4 @ X1 @ X1)))) )),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f191])).
% 0.22/0.32 thf(f197,plain,(
% 0.22/0.32 ( ! [X0 : a] : (($false = $true) | ($true = ((sF12 @ X0 @ X0)))) )),
% 0.22/0.32 inference(constrained_superposition,[],[f50,f192])).
% 0.22/0.32 thf(f203,plain,(
% 0.22/0.32 ( ! [X0 : a] : (($true = ((sF12 @ X0 @ X0)))) )),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f197])).
% 0.22/0.32 thf(f210,plain,(
% 0.22/0.32 ( ! [X0 : a,X1 : a] : ((((sF13 @ X0 @ X1)) = $true) | ($false = $true) | ($true != ((sF12 @ X1 @ X0)))) )),
% 0.22/0.32 inference(constrained_superposition,[],[f47,f203])).
% 0.22/0.32 thf(f211,plain,(
% 0.22/0.32 ( ! [X0 : a,X1 : a] : ((((sF13 @ X0 @ X1)) = $true) | ($true != ((sF12 @ X1 @ X0)))) )),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f210])).
% 0.22/0.32 thf(f223,plain,(
% 0.22/0.32 ( ! [X2 : a,X0 : a,X1 : a] : (($true != ((sF12 @ X1 @ X0))) | (((sF12 @ X0 @ X2)) = $true) | ($false = $true) | (((sF12 @ X1 @ X2)) != $true)) )),
% 0.22/0.32 inference(constrained_superposition,[],[f211,f48])).
% 0.22/0.32 thf(f225,plain,(
% 0.22/0.32 ( ! [X2 : a,X0 : a,X1 : a] : ((((sF12 @ X0 @ X2)) = $true) | (((sF12 @ X1 @ X2)) != $true) | ($true != ((sF12 @ X1 @ X0)))) )),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f223])).
% 0.22/0.32 thf(f231,plain,(
% 0.22/0.32 ( ! [X0 : a,X1 : a] : (($true != ((sF12 @ X1 @ X0))) | ($false = $true) | (((cQ @ X1 @ X0)) = $true)) )),
% 0.22/0.32 inference(constrained_superposition,[],[f53,f211])).
% 0.22/0.32 thf(f236,plain,(
% 0.22/0.32 ( ! [X0 : a,X1 : a] : ((((cQ @ X1 @ X0)) = $true) | ($true != ((sF12 @ X1 @ X0)))) )),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f231])).
% 0.22/0.32 thf(f242,plain,(
% 0.22/0.32 ($false = $true) | (((sF12 @ sK7 @ sK8)) != $true) | ~spl17_3),
% 0.22/0.32 inference(constrained_superposition,[],[f67,f236])).
% 0.22/0.32 thf(f244,plain,(
% 0.22/0.32 (((sF12 @ sK7 @ sK8)) != $true) | ~spl17_3),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f242])).
% 0.22/0.32 thf(f249,plain,(
% 0.22/0.32 ($true != $true) | ($false = ((sF12 @ sK7 @ sK8))) | ~spl17_3),
% 0.22/0.32 inference(constrained_superposition,[],[f244,f23])).
% 0.22/0.32 thf(f250,plain,(
% 0.22/0.32 ($false = ((sF12 @ sK7 @ sK8))) | ~spl17_3),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f249])).
% 0.22/0.32 thf(f257,plain,(
% 0.22/0.32 ( ! [X2 : a,X0 : a,X1 : a] : ((((sF12 @ X0 @ X2)) = $true) | (((sF12 @ X1 @ X2)) != $true) | ($false = $true) | ($false = ((cQ @ X1 @ X0)))) )),
% 0.22/0.32 inference(constrained_superposition,[],[f48,f54])).
% 0.22/0.32 thf(f259,plain,(
% 0.22/0.32 ( ! [X2 : a,X0 : a,X1 : a] : (($false = ((cQ @ X1 @ X0))) | (((sF12 @ X0 @ X2)) = $true) | (((sF12 @ X1 @ X2)) != $true)) )),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f257])).
% 0.22/0.32 thf(f265,plain,(
% 0.22/0.32 ( ! [X0 : a] : ((((sF12 @ sK7 @ X0)) = $true) | (((sF12 @ sK8 @ X0)) != $true) | ($false = $true)) ) | ~spl17_6),
% 0.22/0.32 inference(constrained_superposition,[],[f259,f80])).
% 0.22/0.32 thf(f274,plain,(
% 0.22/0.32 ( ! [X0 : a] : ((((sF12 @ sK7 @ X0)) = $true) | (((sF12 @ sK8 @ X0)) != $true)) ) | ~spl17_6),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f265])).
% 0.22/0.32 thf(f281,plain,(
% 0.22/0.32 (((sF12 @ sK8 @ sK8)) != $true) | ($false = $true) | (~spl17_3 | ~spl17_6)),
% 0.22/0.32 inference(constrained_superposition,[],[f274,f250])).
% 0.22/0.32 thf(f291,plain,(
% 0.22/0.32 (((sF12 @ sK8 @ sK8)) != $true) | (~spl17_3 | ~spl17_6)),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f281])).
% 0.22/0.32 thf(f297,plain,(
% 0.22/0.32 $false | (~spl17_3 | ~spl17_6)),
% 0.22/0.32 inference(forward_subsumption_resolution,[],[f291,f203])).
% 0.22/0.32 thf(f298,plain,(
% 0.22/0.32 ~spl17_3 | ~spl17_6),
% 0.22/0.32 inference(avatar_contradiction_clause,[],[f297])).
% 0.22/0.32 thf(f531,plain,(
% 0.22/0.32 ($true != $true) | (((sF12 @ sK6 @ sK6)) != $true) | spl17_9),
% 0.22/0.32 inference(constrained_superposition,[],[f93,f236])).
% 0.22/0.32 thf(f533,plain,(
% 0.22/0.32 (((sF12 @ sK6 @ sK6)) != $true) | spl17_9),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f531])).
% 0.22/0.32 thf(f535,plain,(
% 0.22/0.32 $false | spl17_9),
% 0.22/0.32 inference(forward_subsumption_resolution,[],[f533,f203])).
% 0.22/0.32 thf(f536,plain,(
% 0.22/0.32 spl17_9),
% 0.22/0.32 inference(avatar_contradiction_clause,[],[f535])).
% 0.22/0.32 thf(f587,plain,(
% 0.22/0.32 ( ! [X0 : a] : (($true = ((sF12 @ sK1 @ X0))) | (((sF12 @ sK2 @ X0)) != $true) | ($false = $true)) ) | ~spl17_14),
% 0.22/0.32 inference(constrained_superposition,[],[f259,f116])).
% 0.22/0.32 thf(f588,plain,(
% 0.22/0.32 ( ! [X0 : a] : (($true = ((sF12 @ sK1 @ X0))) | (((sF12 @ sK2 @ X0)) != $true)) ) | ~spl17_14),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f587])).
% 0.22/0.32 thf(f732,plain,(
% 0.22/0.32 (((sF12 @ sK3 @ sK1)) != $true) | ($true != $true) | spl17_15),
% 0.22/0.32 inference(constrained_superposition,[],[f121,f236])).
% 0.22/0.32 thf(f735,plain,(
% 0.22/0.32 (((sF12 @ sK3 @ sK1)) != $true) | spl17_15),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f732])).
% 0.22/0.32 thf(f736,plain,(
% 0.22/0.32 ( ! [X0 : a] : (($true != $true) | ($true != ((sF12 @ X0 @ sK1))) | (((sF12 @ X0 @ sK3)) != $true)) ) | spl17_15),
% 0.22/0.32 inference(constrained_superposition,[],[f735,f225])).
% 0.22/0.32 thf(f740,plain,(
% 0.22/0.32 ( ! [X0 : a] : (($true != ((sF12 @ X0 @ sK1))) | (((sF12 @ X0 @ sK3)) != $true)) ) | spl17_15),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f736])).
% 0.22/0.32 thf(f763,plain,(
% 0.22/0.32 ( ! [X0 : a] : ((((sF12 @ sK2 @ X0)) = $true) | ($false = $true) | ($true != ((sF12 @ sK3 @ X0)))) ) | ~spl17_16),
% 0.22/0.32 inference(constrained_superposition,[],[f259,f127])).
% 0.22/0.32 thf(f764,plain,(
% 0.22/0.32 ( ! [X0 : a] : ((((sF12 @ sK2 @ X0)) = $true) | ($true != ((sF12 @ sK3 @ X0)))) ) | ~spl17_16),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f763])).
% 0.22/0.32 thf(f850,plain,(
% 0.22/0.32 ($true != $true) | (((sF12 @ sK1 @ sK3)) != $true) | spl17_15),
% 0.22/0.32 inference(constrained_superposition,[],[f740,f203])).
% 0.22/0.32 thf(f862,plain,(
% 0.22/0.32 (((sF12 @ sK1 @ sK3)) != $true) | spl17_15),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f850])).
% 0.22/0.32 thf(f869,definition,(
% 0.22/0.32 spl17_25 <=> (((sF12 @ sK1 @ sK3)) = $true)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl17_25])],[avatar_definition])).
% 0.22/0.32 thf(f871,plain,(
% 0.22/0.32 (((sF12 @ sK1 @ sK3)) != $true) | spl17_25),
% 0.22/0.32 inference(avatar_component_clause,[],[f869])).
% 0.22/0.32 thf(f873,plain,(
% 0.22/0.32 ~spl17_25 | spl17_15),
% 0.22/0.32 inference(avatar_split_clause,[],[f862,f119,f869])).
% 0.22/0.32 thf(f882,plain,(
% 0.22/0.32 ($true != $true) | ($true != ((sF12 @ sK2 @ sK3))) | (~spl17_14 | spl17_25)),
% 0.22/0.32 inference(constrained_superposition,[],[f871,f588])).
% 0.22/0.32 thf(f887,plain,(
% 0.22/0.32 ($true != ((sF12 @ sK2 @ sK3))) | (~spl17_14 | spl17_25)),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f882])).
% 0.22/0.32 thf(f904,plain,(
% 0.22/0.32 ($true != $true) | ($true != ((sF12 @ sK3 @ sK3))) | (~spl17_14 | ~spl17_16 | spl17_25)),
% 0.22/0.32 inference(constrained_superposition,[],[f887,f764])).
% 0.22/0.32 thf(f910,plain,(
% 0.22/0.32 ($true != ((sF12 @ sK3 @ sK3))) | (~spl17_14 | ~spl17_16 | spl17_25)),
% 0.22/0.32 inference(trivial_inequality_removal,[],[f904])).
% 0.22/0.32 thf(f912,plain,(
% 0.22/0.32 $false | (~spl17_14 | ~spl17_16 | spl17_25)),
% 0.22/0.32 inference(forward_subsumption_resolution,[],[f910,f203])).
% 0.22/0.32 thf(f913,plain,(
% 0.22/0.32 ~spl17_14 | ~spl17_16 | spl17_25),
% 0.22/0.32 inference(avatar_contradiction_clause,[],[f912])).
% 0.22/0.32 cnf(s2, plain, spl17_3 | spl17_4, inference(sat_conversion,[],[f72])).
% 0.22/0.32 cnf(s3, plain, spl17_5 | spl17_6, inference(sat_conversion,[],[f81])).
% 0.22/0.32 cnf(s6, plain, spl17_11 | spl17_12, inference(sat_conversion,[],[f108])).
% 0.22/0.32 cnf(s7, plain, ~spl17_13 | spl17_14, inference(sat_conversion,[],[f117])).
% 0.22/0.32 cnf(s8, plain, ~spl17_13 | ~spl17_15, inference(sat_conversion,[],[f122])).
% 0.22/0.32 cnf(s9, plain, spl17_7 | ~spl17_11 | spl17_13, inference(sat_conversion,[],[f123])).
% 0.22/0.32 cnf(s10, plain, ~spl17_13 | spl17_16, inference(sat_conversion,[],[f128])).
% 0.22/0.32 cnf(s11, plain, ~spl17_4 | ~spl17_11 | spl17_13, inference(sat_conversion,[],[f129])).
% 0.22/0.32 cnf(s12, plain, ~spl17_5 | ~spl17_7, inference(sat_conversion,[],[f132])).
% 0.22/0.32 cnf(s16, plain, ~spl17_9 | ~spl17_12, inference(sat_conversion,[],[f169])).
% 0.22/0.32 cnf(s22, plain, ~spl17_3 | ~spl17_6, inference(sat_conversion,[],[f298])).
% 0.22/0.32 cnf(s26, plain, spl17_9, inference(sat_conversion,[],[f536])).
% 0.22/0.32 cnf(s43, plain, spl17_15 | ~spl17_25, inference(sat_conversion,[],[f873])).
% 0.22/0.32 cnf(s44, plain, ~spl17_14 | ~spl17_16 | spl17_25, inference(sat_conversion,[],[f913])).
% 0.22/0.32 cnf(s45, plain, ~spl17_12, inference(rat,[],[s16,s26])).
% 0.22/0.32 cnf(s46, plain, spl17_11, inference(rat,[],[s6,s45])).
% 0.22/0.32 cnf(s48, plain, ~spl17_13, inference(rat,[],[s44,s43,s7,s8,s10])).
% 0.22/0.32 cnf(s49, plain, ~spl17_4, inference(rat,[],[s11,s46,s48])).
% 0.22/0.32 cnf(s50, plain, spl17_7, inference(rat,[],[s9,s46,s48])).
% 0.22/0.32 cnf(s52, plain, spl17_3, inference(rat,[],[s2,s49])).
% 0.22/0.32 cnf(s53, plain, ~spl17_5, inference(rat,[],[s12,s50])).
% 0.22/0.32 cnf(s54, plain, ~spl17_6, inference(rat,[],[s22,s52])).
% 0.22/0.32 cnf(s56, plain, $false, inference(rat,[],[s3,s54,s53])).
% 0.22/0.32 thf(f914,plain,(
% 0.22/0.32 $false),
% 0.22/0.32 inference(avatar_sat_refutation,[],[s56])).
% 0.22/0.32 % SZS output end Proof for theBenchmark
% 0.22/0.32 % (4131230)------------------------------
% 0.22/0.32 % (4131230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.32 % (4131230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.32 % (4131230)CaDiCaL version: 2.1.3
% 0.22/0.32 % (4131230)Termination reason: Refutation
% 0.22/0.32 % (4131230)Time elapsed: 0.030 s
% 0.22/0.32 % (4131230)Peak memory usage: 13 MB
% 0.22/0.32 % (4131230)Instructions burned: 52 (million)
% 0.22/0.32 % (4131219)Success in time 0.069 s
% 0.22/0.32 % Vampire exiting
%------------------------------------------------------------------------------