%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET671^3 : TPTP v9.3.1. Released v3.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:23:27 AM UTC 2026
% Result : Theorem 0.22s 0.29s
% Output : Refutation 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET671^3 : TPTP v9.3.1. Released v3.6.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n010.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 13:41:04 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.09/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.22/0.29 % (2868532)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.22/0.29 % (2868540)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=2581078269: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.29 % (2868543)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.29 % (2868543)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.29 % (2868541)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=895742037:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.22/0.29 % (2868537)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2450781821:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.22/0.29 % (2868538)lrs+10_16_si=on:nwc=1.5:random_seed=2220026181:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.22/0.29 % (2868539)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2289207649:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.22/0.29 % (2868542)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3604577121:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.22/0.29 % (2868543)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=718303485:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.22/0.29 % (2868539)Instruction limit reached!
% 0.22/0.29 % (2868539)------------------------------
% 0.22/0.29 % (2868539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.29 % (2868539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.29 % (2868539)CaDiCaL version: 2.1.3
% 0.22/0.29 % (2868539)Termination reason: Instruction limit
% 0.22/0.29 % (2868539)Termination phase: Property scanning
% 0.22/0.29 % (2868539)Time elapsed: 0.002 s
% 0.22/0.29 % (2868539)Peak memory usage: 9 MB
% 0.22/0.29 % (2868539)Instructions burned: 4 (million)
% 0.22/0.29 % (2868540) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2868532-2868540"...
% 0.22/0.29 % (2868540)...printing done.
% 0.22/0.29 % (2868540)Refutation found. Thanks to Tanya!
% 0.22/0.29 % SZS status Theorem for theBenchmark
% 0.22/0.29 % SZS output start Proof for theBenchmark
% 0.22/0.29 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.22/0.29 thf(func_def_0, type, in: ($i > ($i > $o) > $o)).
% 0.22/0.29 thf(func_def_2, type, is_a: ($i > ($i > $o) > $o)).
% 0.22/0.29 thf(func_def_3, type, emptyset: ($i > $o)).
% 0.22/0.29 thf(func_def_4, type, unord_pair: ($i > $i > $i > $o)).
% 0.22/0.29 thf(func_def_5, type, singleton: ($i > $i > $o)).
% 0.22/0.29 thf(func_def_6, type, union: (($i > $o) > ($i > $o) > $i > $o)).
% 0.22/0.29 thf(func_def_7, type, excl_union: (($i > $o) > ($i > $o) > $i > $o)).
% 0.22/0.29 thf(func_def_8, type, intersection: (($i > $o) > ($i > $o) > $i > $o)).
% 0.22/0.29 thf(func_def_9, type, setminus: (($i > $o) > ($i > $o) > $i > $o)).
% 0.22/0.29 thf(func_def_10, type, complement: (($i > $o) > $i > $o)).
% 0.22/0.29 thf(func_def_11, type, disjoint: (($i > $o) > ($i > $o) > $o)).
% 0.22/0.29 thf(func_def_12, type, subset: (($i > $o) > ($i > $o) > $o)).
% 0.22/0.29 thf(func_def_13, type, meets: (($i > $o) > ($i > $o) > $o)).
% 0.22/0.29 thf(func_def_14, type, misses: (($i > $o) > ($i > $o) > $o)).
% 0.22/0.29 thf(func_def_15, type, cartesian_product: (($i > $o) > ($i > $o) > $i > $i > $o)).
% 0.22/0.29 thf(func_def_16, type, pair_rel: ($i > $i > $i > $i > $o)).
% 0.22/0.29 thf(func_def_17, type, id_rel: (($i > $o) > $i > $i > $o)).
% 0.22/0.29 thf(func_def_18, type, sub_rel: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 0.22/0.29 thf(func_def_19, type, is_rel_on: (($i > $i > $o) > ($i > $o) > ($i > $o) > $o)).
% 0.22/0.29 thf(func_def_20, type, restrict_rel_domain: (($i > $i > $o) > ($i > $o) > $i > $i > $o)).
% 0.22/0.29 thf(func_def_21, type, rel_diagonal: ($i > $i > $o)).
% 0.22/0.29 thf(func_def_22, type, rel_composition: (($i > $i > $o) > ($i > $i > $o) > $i > $i > $o)).
% 0.22/0.29 thf(func_def_23, type, reflexive: (($i > $i > $o) > $o)).
% 0.22/0.29 thf(func_def_24, type, irreflexive: (($i > $i > $o) > $o)).
% 0.22/0.29 thf(func_def_25, type, symmetric: (($i > $i > $o) > $o)).
% 0.22/0.29 thf(func_def_26, type, transitive: (($i > $i > $o) > $o)).
% 0.22/0.29 thf(func_def_27, type, equiv_rel: (($i > $i > $o) > $o)).
% 0.22/0.29 thf(func_def_28, type, rel_codomain: (($i > $i > $o) > $i > $o)).
% 0.22/0.29 thf(func_def_29, type, rel_domain: (($i > $i > $o) > $i > $o)).
% 0.22/0.29 thf(func_def_30, type, rel_inverse: (($i > $i > $o) > $i > $i > $o)).
% 0.22/0.29 thf(func_def_31, type, equiv_classes: (($i > $i > $o) > ($i > $o) > $o)).
% 0.22/0.29 thf(func_def_32, type, restrict_rel_codomain: (($i > $i > $o) > ($i > $o) > $i > $i > $o)).
% 0.22/0.29 thf(func_def_33, type, rel_field: (($i > $i > $o) > $i > $o)).
% 0.22/0.29 thf(func_def_34, type, well_founded: (($i > $i > $o) > $o)).
% 0.22/0.29 thf(func_def_35, type, upwards_well_founded: (($i > $i > $o) > $o)).
% 0.22/0.29 thf(func_def_36, type, db0: !>[X0: $tType]:(X0)).
% 0.22/0.29 thf(func_def_37, type, db1: !>[X0: $tType]:(X0)).
% 0.22/0.29 thf(func_def_38, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.22/0.29 thf(func_def_39, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.22/0.29 thf(func_def_40, type, db2: !>[X0: $tType]:(X0)).
% 0.22/0.29 thf(func_def_41, type, vAND: ($o > $o > $o)).
% 0.22/0.29 thf(func_def_42, type, vOR: ($o > $o > $o)).
% 0.22/0.29 thf(func_def_43, type, vNOT: ($o > $o)).
% 0.22/0.29 thf(func_def_44, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.22/0.29 thf(func_def_45, type, db3: !>[X0: $tType]:(X0)).
% 0.22/0.29 thf(func_def_46, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.22/0.29 thf(func_def_47, type, vIMP: ($o > $o > $o)).
% 0.22/0.29 thf(func_def_48, type, db4: !>[X0: $tType]:(X0)).
% 0.22/0.29 thf(func_def_49, type, vIFF: ($o > $o > $o)).
% 0.22/0.29 thf(func_def_52, type, sK0: ($i > $o)).
% 0.22/0.29 thf(func_def_53, type, sK1: ($i > $i > $o)).
% 0.22/0.29 thf(func_def_54, type, sK2: ($i > $o)).
% 0.22/0.29 thf(func_def_55, type, sK3: ($i > $o)).
% 0.22/0.29 thf(func_def_59, type, sK7: (($i > $o) > ($i > $o) > $i)).
% 0.22/0.29 thf(func_def_60, type, sK8: (($i > $o) > ($i > $i > $o) > ($i > $o) > $i)).
% 0.22/0.29 thf(func_def_61, type, sK9: (($i > $o) > ($i > $i > $o) > ($i > $o) > $i)).
% 0.22/0.29 thf(func_def_64, type, sK12: (($i > $i > $o) > $i)).
% 0.22/0.29 thf(func_def_65, type, sK13: (($i > $i > $o) > $i)).
% 0.22/0.29 thf(f12,axiom,(
% 0.22/0.29 ((^[X0 : ($i > $o), X1 : ($i > $o)] : (! [X2 : $i] : ((X0 @ X2) => (X1 @ X2)))) = subset)),
% 0.22/0.29 file('/export/starexec/sandbox/benchmark/Axioms/SET008^0.ax',subset)).
% 0.22/0.29 thf(f19,axiom,(
% 0.22/0.29 (is_rel_on = (^[X0 : ($i > $i > $o), X1 : ($i > $o), X2 : ($i > $o)] : (! [X4 : $i,X3 : $i] : ((X0 @ X3 @ X4) => ((X1 @ X3) & (X2 @ X4))))))),
% 0.22/0.29 file('/export/starexec/sandbox/benchmark/Axioms/SET008^2.ax',is_rel_on)).
% 0.22/0.29 thf(f20,axiom,(
% 0.22/0.29 ((^[X0 : ($i > $i > $o), X1 : ($i > $o), X2 : $i, X3 : $i] : ((X1 @ X2) & (X0 @ X2 @ X3))) = restrict_rel_domain)),
% 0.22/0.29 file('/export/starexec/sandbox/benchmark/Axioms/SET008^2.ax',restrict_rel_domain)).
% 0.22/0.29 thf(f36,conjecture,(
% 0.22/0.29 ! [X3 : ($i > $o),X1 : ($i > $i > $o),X2 : ($i > $o),X0 : ($i > $o)] : (((is_rel_on @ X1 @ X2 @ X3) & (subset @ X2 @ X0)) => (((restrict_rel_domain @ X1 @ X0)) = X1))),
% 0.22/0.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm)).
% 0.22/0.29 thf(f37,negated_conjecture,(
% 0.22/0.29 ~ ! [X3 : ($i > $o),X1 : ($i > $i > $o),X2 : ($i > $o),X0 : ($i > $o)] : (((is_rel_on @ X1 @ X2 @ X3) & (subset @ X2 @ X0)) => (((restrict_rel_domain @ X1 @ X0)) = X1))),
% 0.22/0.29 inference(negated_conjecture,[status(cth)],[f36])).
% 0.22/0.29 thf(f51,plain,(
% 0.22/0.29 ((^[X0 : ($i > $o), X1 : ($i > $o)] : (! [X2 : $i] : ((X0 @ X2) => (X1 @ X2)))) = subset)),
% 0.22/0.29 inference(rectify,[],[f12])).
% 0.22/0.29 thf(f52,plain,(
% 0.22/0.29 (subset = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (Y1 @ Y2))))))))),
% 0.22/0.29 inference(fool_elimination,[],[f51])).
% 0.22/0.29 thf(f55,plain,(
% 0.22/0.29 (is_rel_on = (^[X0 : ($i > $i > $o), X1 : ($i > $o), X2 : ($i > $o)] : (! [X3 : $i,X4 : $i] : ((X0 @ X4 @ X3) => ((X1 @ X4) & (X2 @ X3))))))),
% 0.22/0.29 inference(rectify,[],[f19])).
% 0.22/0.29 thf(f56,plain,(
% 0.22/0.29 (is_rel_on = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y0 @ Y3 @ Y4) => ((Y2 @ Y4) & (Y1 @ Y3)))))))))))))),
% 0.22/0.29 inference(fool_elimination,[],[f55])).
% 0.22/0.29 thf(f86,plain,(
% 0.22/0.29 ~ ! [X0 : ($i > $o),X1 : ($i > $i > $o),X2 : ($i > $o),X3 : ($i > $o)] : (((is_rel_on @ X1 @ X2 @ X0) & (subset @ X2 @ X3)) => (((restrict_rel_domain @ X1 @ X3)) = X1))),
% 0.22/0.29 inference(rectify,[],[f37])).
% 0.22/0.29 thf(f87,plain,(
% 0.22/0.29 ~ ! [X0 : ($i > $o),X1 : ($i > $i > $o),X2 : ($i > $o),X3 : ($i > $o)] : ((($true = ((subset @ X2 @ X3))) & ($true = ((is_rel_on @ X1 @ X2 @ X0)))) => (((restrict_rel_domain @ X1 @ X3)) = X1))),
% 0.22/0.29 inference(fool_elimination,[],[f86])).
% 0.22/0.29 thf(f89,plain,(
% 0.22/0.29 ((^[X0 : ($i > $i > $o), X1 : ($i > $o), X2 : $i, X3 : $i] : ((X1 @ X2) & (X0 @ X2 @ X3))) = restrict_rel_domain)),
% 0.22/0.29 inference(rectify,[],[f20])).
% 0.22/0.29 thf(f90,plain,(
% 0.22/0.29 (restrict_rel_domain = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((Y0 @ Y2 @ Y3) & (Y1 @ Y2))))))))))),
% 0.22/0.29 inference(fool_elimination,[],[f89])).
% 0.22/0.29 thf(f101,plain,(
% 0.22/0.29 ? [X0 : ($i > $o),X1 : ($i > $i > $o),X2 : ($i > $o),X3 : ($i > $o)] : ((((restrict_rel_domain @ X1 @ X3)) != X1) & (($true = ((subset @ X2 @ X3))) & ($true = ((is_rel_on @ X1 @ X2 @ X0)))))),
% 0.22/0.29 inference(ennf_transformation,[],[f87])).
% 0.22/0.29 thf(f102,plain,(
% 0.22/0.29 ? [X2 : ($i > $o),X1 : ($i > $i > $o),X3 : ($i > $o),X0 : ($i > $o)] : (($true = ((is_rel_on @ X1 @ X2 @ X0))) & ($true = ((subset @ X2 @ X3))) & (((restrict_rel_domain @ X1 @ X3)) != X1))),
% 0.22/0.29 inference(flattening,[],[f101])).
% 0.22/0.29 thf(f103,plain,(
% 0.22/0.29 ? [X0 : ($i > $o),X1 : ($i > $i > $o),X2 : ($i > $o),X3 : ($i > $o)] : (($true = ((is_rel_on @ X1 @ X0 @ X3))) & (((subset @ X0 @ X2)) = $true) & (((restrict_rel_domain @ X1 @ X2)) != X1))),
% 0.22/0.29 inference(rectify,[],[f102])).
% 0.22/0.29 thf(f104,plain,(
% 0.22/0.29 ($true = ((is_rel_on @ sK1 @ sK0 @ sK3))) & ($true = ((subset @ sK0 @ sK2))) & (sK1 != ((restrict_rel_domain @ sK1 @ sK2)))),
% 0.22/0.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f103])).
% 0.22/0.29 thf(f108,plain,(
% 0.22/0.29 (is_rel_on = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y0 @ Y3 @ Y4) => ((Y2 @ Y4) & (Y1 @ Y3)))))))))))))),
% 0.22/0.29 inference(cnf_transformation,[],[f56])).
% 0.22/0.29 thf(f114,plain,(
% 0.22/0.29 (sK1 != ((restrict_rel_domain @ sK1 @ sK2)))),
% 0.22/0.29 inference(cnf_transformation,[],[f104])).
% 0.22/0.29 thf(f115,plain,(
% 0.22/0.29 ($true = ((subset @ sK0 @ sK2)))),
% 0.22/0.29 inference(cnf_transformation,[],[f104])).
% 0.22/0.29 thf(f116,plain,(
% 0.22/0.29 ($true = ((is_rel_on @ sK1 @ sK0 @ sK3)))),
% 0.22/0.29 inference(cnf_transformation,[],[f104])).
% 0.22/0.29 thf(f120,plain,(
% 0.22/0.29 (subset = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (Y1 @ Y2))))))))),
% 0.22/0.29 inference(cnf_transformation,[],[f52])).
% 0.22/0.29 thf(f130,plain,(
% 0.22/0.29 (restrict_rel_domain = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((Y0 @ Y2 @ Y3) & (Y1 @ Y2))))))))))),
% 0.22/0.29 inference(cnf_transformation,[],[f90])).
% 0.22/0.29 thf(f173,definition,(
% 0.22/0.29 spl4_6 <=> (subset = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (Y1 @ Y2))))))))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition])).
% 0.22/0.29 thf(f175,plain,(
% 0.22/0.29 (subset = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (Y1 @ Y2)))))))) | ~spl4_6),
% 0.22/0.29 inference(avatar_component_clause,[],[f173])).
% 0.22/0.29 thf(f176,plain,(
% 0.22/0.29 spl4_6),
% 0.22/0.29 inference(avatar_split_clause,[],[f120,f173])).
% 0.22/0.29 thf(f178,definition,(
% 0.22/0.29 spl4_7 <=> (is_rel_on = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y0 @ Y3 @ Y4) => ((Y2 @ Y4) & (Y1 @ Y3)))))))))))))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_7])],[avatar_definition])).
% 0.22/0.29 thf(f180,plain,(
% 0.22/0.29 (is_rel_on = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y0 @ Y3 @ Y4) => ((Y2 @ Y4) & (Y1 @ Y3))))))))))))) | ~spl4_7),
% 0.22/0.29 inference(avatar_component_clause,[],[f178])).
% 0.22/0.29 thf(f181,plain,(
% 0.22/0.29 spl4_7),
% 0.22/0.29 inference(avatar_split_clause,[],[f108,f178])).
% 0.22/0.29 thf(f208,definition,(
% 0.22/0.29 spl4_13 <=> (sK1 = ((restrict_rel_domain @ sK1 @ sK2)))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition])).
% 0.22/0.29 thf(f210,plain,(
% 0.22/0.29 (sK1 != ((restrict_rel_domain @ sK1 @ sK2))) | spl4_13),
% 0.22/0.29 inference(avatar_component_clause,[],[f208])).
% 0.22/0.29 thf(f211,plain,(
% 0.22/0.29 ~spl4_13),
% 0.22/0.29 inference(avatar_split_clause,[],[f114,f208])).
% 0.22/0.29 thf(f248,definition,(
% 0.22/0.29 spl4_21 <=> ($true = ((is_rel_on @ sK1 @ sK0 @ sK3)))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_21])],[avatar_definition])).
% 0.22/0.29 thf(f250,plain,(
% 0.22/0.29 ($true = ((is_rel_on @ sK1 @ sK0 @ sK3))) | ~spl4_21),
% 0.22/0.29 inference(avatar_component_clause,[],[f248])).
% 0.22/0.29 thf(f251,plain,(
% 0.22/0.29 spl4_21),
% 0.22/0.29 inference(avatar_split_clause,[],[f116,f248])).
% 0.22/0.29 thf(f258,definition,(
% 0.22/0.29 spl4_23 <=> ($true = ((subset @ sK0 @ sK2)))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_23])],[avatar_definition])).
% 0.22/0.29 thf(f260,plain,(
% 0.22/0.29 ($true = ((subset @ sK0 @ sK2))) | ~spl4_23),
% 0.22/0.29 inference(avatar_component_clause,[],[f258])).
% 0.22/0.29 thf(f261,plain,(
% 0.22/0.29 spl4_23),
% 0.22/0.29 inference(avatar_split_clause,[],[f115,f258])).
% 0.22/0.29 thf(f293,definition,(
% 0.22/0.29 spl4_30 <=> (restrict_rel_domain = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((Y0 @ Y2 @ Y3) & (Y1 @ Y2))))))))))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_30])],[avatar_definition])).
% 0.22/0.29 thf(f295,plain,(
% 0.22/0.29 (restrict_rel_domain = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((Y0 @ Y2 @ Y3) & (Y1 @ Y2)))))))))) | ~spl4_30),
% 0.22/0.29 inference(avatar_component_clause,[],[f293])).
% 0.22/0.29 thf(f296,plain,(
% 0.22/0.29 spl4_30),
% 0.22/0.29 inference(avatar_split_clause,[],[f130,f293])).
% 0.22/0.29 thf(f337,plain,(
% 0.22/0.29 (((restrict_rel_domain @ sK1 @ sK2 @ sK5)) != ((sK1 @ sK5))) | spl4_13),
% 0.22/0.29 inference(negative_extensionality,[],[f210])).
% 0.22/0.29 thf(f339,definition,(
% 0.22/0.29 spl4_39 <=> (((restrict_rel_domain @ sK1 @ sK2 @ sK5)) = ((sK1 @ sK5)))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_39])],[avatar_definition])).
% 0.22/0.29 thf(f341,plain,(
% 0.22/0.29 (((restrict_rel_domain @ sK1 @ sK2 @ sK5)) != ((sK1 @ sK5))) | spl4_39),
% 0.22/0.29 inference(avatar_component_clause,[],[f339])).
% 0.22/0.29 thf(f342,plain,(
% 0.22/0.29 ~spl4_39 | spl4_13),
% 0.22/0.29 inference(avatar_split_clause,[],[f337,f208,f339])).
% 0.22/0.29 thf(f350,plain,(
% 0.22/0.29 (((sK1 @ sK5 @ sK6)) != ((restrict_rel_domain @ sK1 @ sK2 @ sK5 @ sK6))) | spl4_39),
% 0.22/0.29 inference(negative_extensionality,[],[f341])).
% 0.22/0.29 thf(f351,plain,(
% 0.22/0.29 ($true = ((restrict_rel_domain @ sK1 @ sK2 @ sK5 @ sK6))) | (((sK1 @ sK5 @ sK6)) = $true) | spl4_39),
% 0.22/0.29 inference(xor_proxy_clausification,[],[f350])).
% 0.22/0.29 thf(f352,plain,(
% 0.22/0.29 ($false = ((sK1 @ sK5 @ sK6))) | ($false = ((restrict_rel_domain @ sK1 @ sK2 @ sK5 @ sK6))) | spl4_39),
% 0.22/0.29 inference(xor_proxy_clausification,[],[f350])).
% 0.22/0.29 thf(f354,definition,(
% 0.22/0.29 spl4_40 <=> ($false = ((restrict_rel_domain @ sK1 @ sK2 @ sK5 @ sK6)))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_40])],[avatar_definition])).
% 0.22/0.29 thf(f356,plain,(
% 0.22/0.29 ($false = ((restrict_rel_domain @ sK1 @ sK2 @ sK5 @ sK6))) | ~spl4_40),
% 0.22/0.29 inference(avatar_component_clause,[],[f354])).
% 0.22/0.29 thf(f358,definition,(
% 0.22/0.29 spl4_41 <=> ($false = ((sK1 @ sK5 @ sK6)))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_41])],[avatar_definition])).
% 0.22/0.29 thf(f360,plain,(
% 0.22/0.29 ($false = ((sK1 @ sK5 @ sK6))) | ~spl4_41),
% 0.22/0.29 inference(avatar_component_clause,[],[f358])).
% 0.22/0.29 thf(f361,plain,(
% 0.22/0.29 spl4_40 | spl4_41 | spl4_39),
% 0.22/0.29 inference(avatar_split_clause,[],[f352,f339,f358,f354])).
% 0.22/0.29 thf(f363,definition,(
% 0.22/0.29 spl4_42 <=> (((sK1 @ sK5 @ sK6)) = $true)),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_42])],[avatar_definition])).
% 0.22/0.29 thf(f365,plain,(
% 0.22/0.29 (((sK1 @ sK5 @ sK6)) = $true) | ~spl4_42),
% 0.22/0.29 inference(avatar_component_clause,[],[f363])).
% 0.22/0.29 thf(f367,definition,(
% 0.22/0.29 spl4_43 <=> ($true = ((restrict_rel_domain @ sK1 @ sK2 @ sK5 @ sK6)))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_43])],[avatar_definition])).
% 0.22/0.29 thf(f369,plain,(
% 0.22/0.29 ($true = ((restrict_rel_domain @ sK1 @ sK2 @ sK5 @ sK6))) | ~spl4_43),
% 0.22/0.29 inference(avatar_component_clause,[],[f367])).
% 0.22/0.29 thf(f370,plain,(
% 0.22/0.29 spl4_42 | spl4_43 | spl4_39),
% 0.22/0.29 inference(avatar_split_clause,[],[f351,f339,f367,f363])).
% 0.22/0.29 thf(f371,plain,(
% 0.22/0.29 ($false = $true) | (~spl4_41 | ~spl4_42)),
% 0.22/0.29 inference(forward_demodulation,[],[f365,f360])).
% 0.22/0.29 thf(f372,plain,(
% 0.22/0.29 $false | (~spl4_41 | ~spl4_42)),
% 0.22/0.29 inference(trivial_inequality_removal,[],[f371])).
% 0.22/0.29 thf(f373,plain,(
% 0.22/0.29 ~spl4_41 | ~spl4_42),
% 0.22/0.29 inference(avatar_contradiction_clause,[],[f372])).
% 0.22/0.29 thf(f379,plain,(
% 0.22/0.29 ( ! [X1 : ($i > $o)] : ((((subset @ X1)) = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (Y1 @ Y2))))))) @ X1)))) ) | ~spl4_6),
% 0.22/0.29 inference(argument_congruence,[],[f175])).
% 0.22/0.29 thf(f380,plain,(
% 0.22/0.29 ( ! [X1 : ($i > $o)] : ((((subset @ X1)) = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: ((X1 @ Y1) => (Y0 @ Y1))))))) ) | ~spl4_6),
% 0.22/0.29 inference(beta-eta_normalization,[],[f379])).
% 0.22/0.29 thf(f381,plain,(
% 0.22/0.29 ( ! [X1 : ($i > $i > $o)] : ((((restrict_rel_domain @ X1)) = (((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((Y0 @ Y2 @ Y3) & (Y1 @ Y2))))))))) @ X1)))) ) | ~spl4_30),
% 0.22/0.29 inference(argument_congruence,[],[f295])).
% 0.22/0.29 thf(f382,plain,(
% 0.22/0.29 ( ! [X1 : ($i > $i > $o)] : ((((restrict_rel_domain @ X1)) = (^[Y0 : $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((X1 @ Y1 @ Y2) & (Y0 @ Y1))))))))) ) | ~spl4_30),
% 0.22/0.29 inference(beta-eta_normalization,[],[f381])).
% 0.22/0.29 thf(f383,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X1 : ($i > $o)] : (((((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: ((X1 @ Y1) => (Y0 @ Y1))))) @ X2)) = ((subset @ X1 @ X2)))) ) | ~spl4_6),
% 0.22/0.29 inference(argument_congruence,[],[f380])).
% 0.22/0.29 thf(f384,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X1 : ($i > $o)] : (($false = ((subset @ X1 @ X2))) | ((((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: ((X1 @ Y1) => (Y0 @ Y1))))) @ X2)) = $true)) ) | ~spl4_6),
% 0.22/0.29 inference(iff_proxy_clausification,[],[f383])).
% 0.22/0.29 thf(f391,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X1 : ($i > $o)] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((X1 @ Y0) => (X2 @ Y0)))))) | ($false = ((subset @ X1 @ X2)))) ) | ~spl4_6),
% 0.22/0.29 inference(beta-eta_normalization,[],[f384])).
% 0.22/0.29 thf(f392,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o)] : (($false = ((subset @ X1 @ X2))) | ($true = (((^[Y0 : $i]: ((X1 @ Y0) => (X2 @ Y0))) @ X3)))) ) | ~spl4_6),
% 0.22/0.29 inference(pi_proxy_clausification,[],[f391])).
% 0.22/0.29 thf(f393,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o)] : (($true = (((X1 @ X3) => (X2 @ X3)))) | ($false = ((subset @ X1 @ X2)))) ) | ~spl4_6),
% 0.22/0.29 inference(beta-eta_normalization,[],[f392])).
% 0.22/0.29 thf(f394,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o)] : (($false = ((subset @ X1 @ X2))) | (((X1 @ X3)) = $false) | ($true = ((X2 @ X3)))) ) | ~spl4_6),
% 0.22/0.29 inference(imp_proxy_clausification,[],[f393])).
% 0.22/0.29 thf(f395,plain,(
% 0.22/0.29 ( ! [X1 : ($i > $i > $o)] : ((((is_rel_on @ X1)) = (((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y0 @ Y3 @ Y4) => ((Y2 @ Y4) & (Y1 @ Y3)))))))))))) @ X1)))) ) | ~spl4_7),
% 0.22/0.29 inference(argument_congruence,[],[f180])).
% 0.22/0.29 thf(f396,plain,(
% 0.22/0.29 ( ! [X1 : ($i > $i > $o)] : ((((is_rel_on @ X1)) = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((X1 @ Y2 @ Y3) => ((Y1 @ Y3) & (Y0 @ Y2)))))))))))) ) | ~spl4_7),
% 0.22/0.29 inference(beta-eta_normalization,[],[f395])).
% 0.22/0.29 thf(f400,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X1 : ($i > $i > $o)] : (((((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((X1 @ Y1 @ Y2) & (Y0 @ Y1))))))) @ X2)) = ((restrict_rel_domain @ X1 @ X2)))) ) | ~spl4_30),
% 0.22/0.29 inference(argument_congruence,[],[f382])).
% 0.22/0.29 thf(f401,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X1 : ($i > $i > $o)] : ((((restrict_rel_domain @ X1 @ X2)) = (^[Y0 : $i]: ((^[Y1 : $i]: ((X1 @ Y0 @ Y1) & (X2 @ Y0))))))) ) | ~spl4_30),
% 0.22/0.29 inference(beta-eta_normalization,[],[f400])).
% 0.22/0.29 thf(f402,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X1 : ($i > $i > $o)] : ((((is_rel_on @ X1 @ X2)) = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((X1 @ Y2 @ Y3) => ((Y1 @ Y3) & (Y0 @ Y2)))))))))) @ X2)))) ) | ~spl4_7),
% 0.22/0.29 inference(argument_congruence,[],[f396])).
% 0.22/0.29 thf(f403,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X1 : ($i > $i > $o)] : ((((is_rel_on @ X1 @ X2)) = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((X1 @ Y1 @ Y2) => ((Y0 @ Y2) & (X2 @ Y1)))))))))) ) | ~spl4_7),
% 0.22/0.29 inference(beta-eta_normalization,[],[f402])).
% 0.22/0.29 thf(f405,plain,(
% 0.22/0.29 (sK1 != (^[Y0 : $i]: ((^[Y1 : $i]: ((sK1 @ Y0 @ Y1) & (sK2 @ Y0)))))) | (spl4_13 | ~spl4_30)),
% 0.22/0.29 inference(superposition,[],[f210,f401])).
% 0.22/0.29 thf(f408,definition,(
% 0.22/0.29 spl4_44 <=> (sK1 = (^[Y0 : $i]: ((^[Y1 : $i]: ((sK1 @ Y0 @ Y1) & (sK2 @ Y0))))))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_44])],[avatar_definition])).
% 0.22/0.29 thf(f410,plain,(
% 0.22/0.29 (sK1 != (^[Y0 : $i]: ((^[Y1 : $i]: ((sK1 @ Y0 @ Y1) & (sK2 @ Y0)))))) | spl4_44),
% 0.22/0.29 inference(avatar_component_clause,[],[f408])).
% 0.22/0.29 thf(f411,plain,(
% 0.22/0.29 ~spl4_44 | spl4_13 | ~spl4_30),
% 0.22/0.29 inference(avatar_split_clause,[],[f405,f293,f208,f408])).
% 0.22/0.29 thf(f412,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X3 : ($i > $o),X1 : ($i > $i > $o)] : ((((is_rel_on @ X1 @ X2 @ X3)) = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((X1 @ Y1 @ Y2) => ((Y0 @ Y2) & (X2 @ Y1)))))))) @ X3)))) ) | ~spl4_7),
% 0.22/0.29 inference(argument_congruence,[],[f403])).
% 0.22/0.29 thf(f414,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X3 : ($i > $o),X1 : ($i > $i > $o)] : (((((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((X1 @ Y1 @ Y2) => ((Y0 @ Y2) & (X2 @ Y1)))))))) @ X3)) = $true) | (((is_rel_on @ X1 @ X2 @ X3)) = $false)) ) | ~spl4_7),
% 0.22/0.29 inference(iff_proxy_clausification,[],[f412])).
% 0.22/0.29 thf(f415,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X3 : ($i > $o),X1 : ($i > $i > $o)] : ((((is_rel_on @ X1 @ X2 @ X3)) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((X1 @ Y0 @ Y1) => ((X3 @ Y1) & (X2 @ Y0)))))))))) ) | ~spl4_7),
% 0.22/0.29 inference(beta-eta_normalization,[],[f414])).
% 0.22/0.29 thf(f416,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X3 : ($i > $o),X1 : ($i > $i > $o),X4 : $i] : ((((is_rel_on @ X1 @ X2 @ X3)) = $false) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((X1 @ Y0 @ Y1) => ((X3 @ Y1) & (X2 @ Y0)))))) @ X4)) = $true)) ) | ~spl4_7),
% 0.22/0.29 inference(pi_proxy_clausification,[],[f415])).
% 0.22/0.29 thf(f417,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X3 : ($i > $o),X1 : ($i > $i > $o),X4 : $i] : ((((is_rel_on @ X1 @ X2 @ X3)) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((X1 @ X4 @ Y0) => ((X3 @ Y0) & (X2 @ X4)))))))) ) | ~spl4_7),
% 0.22/0.29 inference(beta-eta_normalization,[],[f416])).
% 0.22/0.29 thf(f418,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X3 : ($i > $o),X1 : ($i > $i > $o),X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: ((X1 @ X4 @ Y0) => ((X3 @ Y0) & (X2 @ X4)))) @ X5))) | (((is_rel_on @ X1 @ X2 @ X3)) = $false)) ) | ~spl4_7),
% 0.22/0.29 inference(pi_proxy_clausification,[],[f417])).
% 0.22/0.29 thf(f419,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X3 : ($i > $o),X1 : ($i > $i > $o),X4 : $i,X5 : $i] : (($true = (((X1 @ X4 @ X5) => ((X3 @ X5) & (X2 @ X4))))) | (((is_rel_on @ X1 @ X2 @ X3)) = $false)) ) | ~spl4_7),
% 0.22/0.29 inference(beta-eta_normalization,[],[f418])).
% 0.22/0.29 thf(f420,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X3 : ($i > $o),X1 : ($i > $i > $o),X4 : $i,X5 : $i] : (($false = ((X1 @ X4 @ X5))) | ((((X3 @ X5) & (X2 @ X4))) = $true) | (((is_rel_on @ X1 @ X2 @ X3)) = $false)) ) | ~spl4_7),
% 0.22/0.29 inference(imp_proxy_clausification,[],[f419])).
% 0.22/0.29 thf(f421,plain,(
% 0.22/0.29 ( ! [X2 : ($i > $o),X3 : ($i > $o),X1 : ($i > $i > $o),X4 : $i,X5 : $i] : ((((is_rel_on @ X1 @ X2 @ X3)) = $false) | (((X2 @ X4)) = $true) | ($false = ((X1 @ X4 @ X5)))) ) | ~spl4_7),
% 0.22/0.29 inference(and_proxy_clausification,[],[f420])).
% 0.22/0.29 thf(f433,plain,(
% 0.22/0.29 ((((^[Y0 : $i]: ((^[Y1 : $i]: ((sK1 @ Y0 @ Y1) & (sK2 @ Y0))))) @ sK10)) != ((sK1 @ sK10))) | spl4_44),
% 0.22/0.29 inference(negative_extensionality,[],[f410])).
% 0.22/0.29 thf(f434,plain,(
% 0.22/0.29 ((^[Y0 : $i]: ((sK1 @ sK10 @ Y0) & (sK2 @ sK10))) != ((sK1 @ sK10))) | spl4_44),
% 0.22/0.29 inference(beta-eta_normalization,[],[f433])).
% 0.22/0.29 thf(f436,definition,(
% 0.22/0.29 spl4_45 <=> ((^[Y0 : $i]: ((sK1 @ sK10 @ Y0) & (sK2 @ sK10))) = ((sK1 @ sK10)))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_45])],[avatar_definition])).
% 0.22/0.29 thf(f438,plain,(
% 0.22/0.29 ((^[Y0 : $i]: ((sK1 @ sK10 @ Y0) & (sK2 @ sK10))) != ((sK1 @ sK10))) | spl4_45),
% 0.22/0.29 inference(avatar_component_clause,[],[f436])).
% 0.22/0.29 thf(f439,plain,(
% 0.22/0.29 ~spl4_45 | spl4_44),
% 0.22/0.29 inference(avatar_split_clause,[],[f434,f408,f436])).
% 0.22/0.29 thf(f440,plain,(
% 0.22/0.29 ( ! [X0 : $i] : ((((sK2 @ X0)) = $true) | ($false = $true) | ($false = ((sK0 @ X0)))) ) | (~spl4_6 | ~spl4_23)),
% 0.22/0.29 inference(superposition,[],[f394,f260])).
% 0.22/0.29 thf(f442,plain,(
% 0.22/0.29 ( ! [X0 : $i] : (($false = ((sK0 @ X0))) | (((sK2 @ X0)) = $true)) ) | (~spl4_6 | ~spl4_23)),
% 0.22/0.29 inference(trivial_inequality_removal,[],[f440])).
% 0.22/0.29 thf(f484,plain,(
% 0.22/0.29 ((((^[Y0 : $i]: ((sK1 @ sK10 @ Y0) & (sK2 @ sK10))) @ sK11)) != ((sK1 @ sK10 @ sK11))) | spl4_45),
% 0.22/0.29 inference(negative_extensionality,[],[f438])).
% 0.22/0.29 thf(f485,plain,(
% 0.22/0.29 ($true = ((sK1 @ sK10 @ sK11))) | ((((^[Y0 : $i]: ((sK1 @ sK10 @ Y0) & (sK2 @ sK10))) @ sK11)) = $true) | spl4_45),
% 0.22/0.29 inference(xor_proxy_clausification,[],[f484])).
% 0.22/0.29 thf(f486,plain,(
% 0.22/0.29 ($false = ((sK1 @ sK10 @ sK11))) | ($false = (((^[Y0 : $i]: ((sK1 @ sK10 @ Y0) & (sK2 @ sK10))) @ sK11))) | spl4_45),
% 0.22/0.29 inference(xor_proxy_clausification,[],[f484])).
% 0.22/0.29 thf(f487,plain,(
% 0.22/0.29 ($false = (((sK1 @ sK10 @ sK11) & (sK2 @ sK10)))) | ($false = ((sK1 @ sK10 @ sK11))) | spl4_45),
% 0.22/0.29 inference(beta-eta_normalization,[],[f486])).
% 0.22/0.29 thf(f488,plain,(
% 0.22/0.29 ($false = ((sK2 @ sK10))) | ($false = ((sK1 @ sK10 @ sK11))) | ($false = ((sK1 @ sK10 @ sK11))) | spl4_45),
% 0.22/0.29 inference(and_proxy_clausification,[],[f487])).
% 0.22/0.29 thf(f489,plain,(
% 0.22/0.29 ($false = ((sK2 @ sK10))) | ($false = ((sK1 @ sK10 @ sK11))) | spl4_45),
% 0.22/0.29 inference(duplicate_literal_removal,[],[f488])).
% 0.22/0.29 thf(f490,plain,(
% 0.22/0.29 ((((sK1 @ sK10 @ sK11) & (sK2 @ sK10))) = $true) | ($true = ((sK1 @ sK10 @ sK11))) | spl4_45),
% 0.22/0.29 inference(beta-eta_normalization,[],[f485])).
% 0.22/0.29 thf(f492,plain,(
% 0.22/0.29 ($true = ((sK1 @ sK10 @ sK11))) | ($true = ((sK1 @ sK10 @ sK11))) | spl4_45),
% 0.22/0.29 inference(and_proxy_clausification,[],[f490])).
% 0.22/0.29 thf(f493,plain,(
% 0.22/0.29 ($true = ((sK1 @ sK10 @ sK11))) | spl4_45),
% 0.22/0.29 inference(duplicate_literal_removal,[],[f492])).
% 0.22/0.29 thf(f495,definition,(
% 0.22/0.29 spl4_46 <=> ($false = ((sK2 @ sK10)))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_46])],[avatar_definition])).
% 0.22/0.29 thf(f497,plain,(
% 0.22/0.29 ($false = ((sK2 @ sK10))) | ~spl4_46),
% 0.22/0.29 inference(avatar_component_clause,[],[f495])).
% 0.22/0.29 thf(f499,definition,(
% 0.22/0.29 spl4_47 <=> ($false = ((sK1 @ sK10 @ sK11)))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_47])],[avatar_definition])).
% 0.22/0.29 thf(f502,plain,(
% 0.22/0.29 spl4_46 | spl4_47 | spl4_45),
% 0.22/0.29 inference(avatar_split_clause,[],[f489,f436,f499,f495])).
% 0.22/0.29 thf(f504,definition,(
% 0.22/0.29 spl4_48 <=> ($true = ((sK1 @ sK10 @ sK11)))),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_48])],[avatar_definition])).
% 0.22/0.29 thf(f506,plain,(
% 0.22/0.29 ($true = ((sK1 @ sK10 @ sK11))) | ~spl4_48),
% 0.22/0.29 inference(avatar_component_clause,[],[f504])).
% 0.22/0.29 thf(f507,plain,(
% 0.22/0.29 spl4_48 | spl4_45),
% 0.22/0.29 inference(avatar_split_clause,[],[f493,f436,f504])).
% 0.22/0.29 thf(f607,plain,(
% 0.22/0.29 ( ! [X0 : $i,X1 : $i] : (($false = ((sK1 @ X0 @ X1))) | ($false = $true) | ($true = ((sK0 @ X0)))) ) | (~spl4_7 | ~spl4_21)),
% 0.22/0.29 inference(superposition,[],[f421,f250])).
% 0.22/0.29 thf(f609,plain,(
% 0.22/0.29 ( ! [X0 : $i,X1 : $i] : (($false = ((sK1 @ X0 @ X1))) | ($true = ((sK0 @ X0)))) ) | (~spl4_7 | ~spl4_21)),
% 0.22/0.29 inference(trivial_inequality_removal,[],[f607])).
% 0.22/0.29 thf(f615,plain,(
% 0.22/0.29 ($false = $true) | (((sK0 @ sK10)) = $true) | (~spl4_7 | ~spl4_21 | ~spl4_48)),
% 0.22/0.29 inference(superposition,[],[f506,f609])).
% 0.22/0.29 thf(f620,plain,(
% 0.22/0.29 (((sK0 @ sK10)) = $true) | (~spl4_7 | ~spl4_21 | ~spl4_48)),
% 0.22/0.29 inference(trivial_inequality_removal,[],[f615])).
% 0.22/0.29 thf(f629,definition,(
% 0.22/0.29 spl4_51 <=> (((sK0 @ sK10)) = $true)),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl4_51])],[avatar_definition])).
% 0.22/0.29 thf(f631,plain,(
% 0.22/0.29 (((sK0 @ sK10)) = $true) | ~spl4_51),
% 0.22/0.29 inference(avatar_component_clause,[],[f629])).
% 0.22/0.29 thf(f632,plain,(
% 0.22/0.29 spl4_51 | ~spl4_7 | ~spl4_21 | ~spl4_48),
% 0.22/0.29 inference(avatar_split_clause,[],[f620,f504,f248,f178,f629])).
% 0.22/0.29 thf(f633,plain,(
% 0.22/0.29 ($false = $true) | (~spl4_40 | ~spl4_43)),
% 0.22/0.29 inference(forward_demodulation,[],[f369,f356])).
% 0.22/0.29 thf(f634,plain,(
% 0.22/0.29 $false | (~spl4_40 | ~spl4_43)),
% 0.22/0.29 inference(trivial_inequality_removal,[],[f633])).
% 0.22/0.29 thf(f635,plain,(
% 0.22/0.29 ~spl4_40 | ~spl4_43),
% 0.22/0.29 inference(avatar_contradiction_clause,[],[f634])).
% 0.22/0.29 thf(f655,plain,(
% 0.22/0.29 ($false = $true) | ($true = ((sK2 @ sK10))) | (~spl4_6 | ~spl4_23 | ~spl4_51)),
% 0.22/0.29 inference(superposition,[],[f442,f631])).
% 0.22/0.29 thf(f657,plain,(
% 0.22/0.29 ($true = ((sK2 @ sK10))) | (~spl4_6 | ~spl4_23 | ~spl4_51)),
% 0.22/0.29 inference(trivial_inequality_removal,[],[f655])).
% 0.22/0.29 thf(f661,plain,(
% 0.22/0.29 ($false = $true) | (~spl4_6 | ~spl4_23 | ~spl4_46 | ~spl4_51)),
% 0.22/0.29 inference(forward_demodulation,[],[f657,f497])).
% 0.22/0.29 thf(f662,plain,(
% 0.22/0.29 $false | (~spl4_6 | ~spl4_23 | ~spl4_46 | ~spl4_51)),
% 0.22/0.29 inference(trivial_inequality_removal,[],[f661])).
% 0.22/0.29 thf(f663,plain,(
% 0.22/0.29 ~spl4_6 | ~spl4_23 | ~spl4_46 | ~spl4_51),
% 0.22/0.29 inference(avatar_contradiction_clause,[],[f662])).
% 0.22/0.29 thf(f664,definition,(
% 0.22/0.29 ($false != ((sK1 @ sK10 @ sK11))) | ($true != ((sK1 @ sK10 @ sK11))) | ($true != ((restrict_rel_domain @ sK1 @ sK2 @ sK5 @ sK6))) | ($false = ((restrict_rel_domain @ sK1 @ sK2 @ sK5 @ sK6)))),
% 0.22/0.29 introduced(theory,[theory_tautology_sat_conflict])).
% 0.22/0.29 thf(f667,definition,(
% 0.22/0.29 ($false != ((restrict_rel_domain @ sK1 @ sK2 @ sK5 @ sK6))) | ($false != ((sK1 @ sK10 @ sK11))) | ($true != ((sK1 @ sK10 @ sK11))) | ($true = ((restrict_rel_domain @ sK1 @ sK2 @ sK5 @ sK6)))),
% 0.22/0.29 introduced(theory,[theory_tautology_sat_conflict])).
% 0.22/0.29 cnf(s6, plain, spl4_6, inference(sat_conversion,[],[f176])).
% 0.22/0.29 cnf(s7, plain, spl4_7, inference(sat_conversion,[],[f181])).
% 0.22/0.29 cnf(s13, plain, ~spl4_13, inference(sat_conversion,[],[f211])).
% 0.22/0.29 cnf(s21, plain, spl4_21, inference(sat_conversion,[],[f251])).
% 0.22/0.29 cnf(s23, plain, spl4_23, inference(sat_conversion,[],[f261])).
% 0.22/0.29 cnf(s30, plain, spl4_30, inference(sat_conversion,[],[f296])).
% 0.22/0.29 cnf(s39, plain, spl4_13 | ~spl4_39, inference(sat_conversion,[],[f342])).
% 0.22/0.29 cnf(s40, plain, spl4_39 | spl4_40 | spl4_41, inference(sat_conversion,[],[f361])).
% 0.22/0.29 cnf(s41, plain, spl4_39 | spl4_42 | spl4_43, inference(sat_conversion,[],[f370])).
% 0.22/0.29 cnf(s42, plain, ~spl4_41 | ~spl4_42, inference(sat_conversion,[],[f373])).
% 0.22/0.29 cnf(s43, plain, spl4_13 | ~spl4_30 | ~spl4_44, inference(sat_conversion,[],[f411])).
% 0.22/0.29 cnf(s44, plain, spl4_44 | ~spl4_45, inference(sat_conversion,[],[f439])).
% 0.22/0.29 cnf(s45, plain, spl4_45 | spl4_46 | spl4_47, inference(sat_conversion,[],[f502])).
% 0.22/0.29 cnf(s46, plain, spl4_45 | spl4_48, inference(sat_conversion,[],[f507])).
% 0.22/0.29 cnf(s50, plain, ~spl4_7 | ~spl4_21 | ~spl4_48 | spl4_51, inference(sat_conversion,[],[f632])).
% 0.22/0.29 cnf(s52, plain, ~spl4_40 | ~spl4_43, inference(sat_conversion,[],[f635])).
% 0.22/0.29 cnf(s59, plain, ~spl4_6 | ~spl4_23 | ~spl4_46 | ~spl4_51, inference(sat_conversion,[],[f663])).
% 0.22/0.29 cnf(s60, plain, spl4_40 | ~spl4_43 | ~spl4_47 | ~spl4_48, inference(sat_conversion,[],[f664])).
% 0.22/0.29 cnf(s63, plain, ~spl4_40 | spl4_43 | ~spl4_47 | ~spl4_48, inference(sat_conversion,[],[f667])).
% 0.22/0.29 cnf(s64, plain, ~spl4_44, inference(rat,[],[s43,s30,s13])).
% 0.22/0.29 cnf(s65, plain, ~spl4_39, inference(rat,[],[s39,s13])).
% 0.22/0.29 cnf(s66, plain, ~spl4_45, inference(rat,[],[s44,s64])).
% 0.22/0.29 cnf(s67, plain, spl4_48, inference(rat,[],[s46,s66])).
% 0.22/0.29 cnf(s68, plain, spl4_51, inference(rat,[],[s50,s67,s21,s7])).
% 0.22/0.29 cnf(s69, plain, ~spl4_46, inference(rat,[],[s59,s68,s23,s6])).
% 0.22/0.29 cnf(s70, plain, spl4_47, inference(rat,[],[s45,s66,s69])).
% 0.22/0.29 cnf(s71, plain, spl4_40, inference(rat,[],[s42,s41,s40,s60,s65,s70,s67])).
% 0.22/0.29 cnf(s72, plain, spl4_43, inference(rat,[],[s63,s67,s70,s71])).
% 0.22/0.29 cnf(s73, plain, $false, inference(rat,[],[s52,s72,s71])).
% 0.22/0.29 thf(f668,plain,(
% 0.22/0.29 $false),
% 0.22/0.29 inference(avatar_sat_refutation,[],[s73])).
% 0.22/0.29 % SZS output end Proof for theBenchmark
% 0.22/0.29 % (2868540)------------------------------
% 0.22/0.29 % (2868540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.29 % (2868540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.29 % (2868540)CaDiCaL version: 2.1.3
% 0.22/0.29 % (2868540)Termination reason: Refutation
% 0.22/0.29 % (2868540)Time elapsed: 0.012 s
% 0.22/0.29 % (2868540)Peak memory usage: 13 MB
% 0.22/0.29 % (2868540)Instructions burned: 37 (million)
% 0.22/0.29 % (2868532)Success in time 0.042 s
% 0.22/0.29 % Vampire exiting
%------------------------------------------------------------------------------