%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM824^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:19:36 AM UTC 2026
% Result : Theorem 9.53s 1.88s
% Output : Refutation 9.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM824^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n002.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 13:05:37 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.52/1.22 % (1241933)Will run a generic schedule for satisfiability detection.
% 6.52/1.22 % (1241939)% WARNING: option uhcvi not known.
% 6.52/1.22 % (1241939)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=584449028:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.52/1.22 % (1241939)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.52/1.22 % (1241939)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 6.52/1.22 % (1241938)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2109503707_2999 on theBenchmark for (2999ds/0Mi)
% 6.52/1.22 % Exception at run slice level
% 6.52/1.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.52/1.22 % (1241941)dis+10_1_sil=32000:sp=arity:random_seed=2408889679:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.52/1.22 % (1241947)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=975478227:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.52/1.22 % Exception at run slice level
% 6.52/1.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.52/1.22 % (1241942)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3469363188:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.52/1.22 % (1241943)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=441964863:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.52/1.22 % (1241940)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1462568062:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.52/1.22 % (1241942)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.52/1.22 % (1241944)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1090424516:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.52/1.22 % (1241950)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1357964070:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.52/1.22 % (1241942)Instruction limit reached!
% 6.52/1.22 % (1241942)------------------------------
% 6.52/1.22 % (1241942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.22 % (1241942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.22 % (1241942)CaDiCaL version: 2.1.3
% 6.52/1.22 % (1241942)Termination reason: Instruction limit
% 6.52/1.22 % (1241942)Termination phase: Saturation
% 6.52/1.22 % (1241942)Time elapsed: 0.057 s
% 6.52/1.22 % (1241942)Peak memory usage: 12 MB
% 6.52/1.22 % (1241942)Instructions burned: 117 (million)
% 6.52/1.22 % (1241941)Instruction limit reached!
% 6.52/1.22 % (1241941)------------------------------
% 6.52/1.22 % (1241941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.22 % (1241941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.22 % (1241941)CaDiCaL version: 2.1.3
% 6.52/1.22 % (1241941)Termination reason: Instruction limit
% 6.52/1.22 % (1241941)Termination phase: Saturation
% 6.52/1.22 % (1241941)Time elapsed: 0.078 s
% 6.52/1.22 % (1241941)Peak memory usage: 12 MB
% 6.52/1.22 % (1241941)Instructions burned: 103 (million)
% 6.52/1.22 % (1241943)Instruction limit reached!
% 6.52/1.22 % (1241943)------------------------------
% 6.52/1.22 % (1241943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.22 % (1241943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.22 % (1241943)CaDiCaL version: 2.1.3
% 6.52/1.22 % (1241943)Termination reason: Instruction limit
% 6.52/1.22 % (1241943)Termination phase: Saturation
% 6.52/1.22 % (1241943)Time elapsed: 0.081 s
% 6.52/1.22 % (1241943)Peak memory usage: 12 MB
% 6.52/1.22 % (1241943)Instructions burned: 133 (million)
% 6.52/1.22 % (1241950)Instruction limit reached!
% 6.52/1.22 % (1241950)------------------------------
% 6.52/1.22 % (1241950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.22 % (1241950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.22 % (1241950)CaDiCaL version: 2.1.3
% 6.52/1.22 % (1241950)Termination reason: Instruction limit
% 6.52/1.22 % (1241950)Termination phase: Saturation
% 6.52/1.22 % (1241950)Time elapsed: 0.073 s
% 6.52/1.22 % (1241950)Peak memory usage: 12 MB
% 6.52/1.22 % (1241950)Instructions burned: 132 (million)
% 6.52/1.22 % (1241957)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1164897927:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 9.53/1.88 % (1241957)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 9.53/1.88 % (1241957)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 9.53/1.88 % (1241958)ott-21_1_sil=16000:fs=off:random_seed=3612064143:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 9.53/1.88 % (1241960)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=565507531:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 9.53/1.88 % Exception at run slice level
% 9.53/1.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.53/1.88 % (1241959)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1558254486:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 9.53/1.88 % (1241968)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3749225424:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 9.53/1.88 % (1241944)Instruction limit reached!
% 9.53/1.88 % (1241944)------------------------------
% 9.53/1.88 % (1241944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.53/1.88 % (1241944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.53/1.88 % (1241944)CaDiCaL version: 2.1.3
% 9.53/1.88 % (1241944)Termination reason: Instruction limit
% 9.53/1.88 % (1241944)Termination phase: Saturation
% 9.53/1.88 % (1241944)Time elapsed: 0.126 s
% 9.53/1.88 % (1241944)Peak memory usage: 12 MB
% 9.53/1.88 % (1241944)Instructions burned: 160 (million)
% 9.53/1.88 % (1241970)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3552702561:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 9.53/1.88 % Exception at run slice level
% 9.53/1.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.53/1.88 % (1241972)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=627338470:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 9.53/1.88 % (1241972)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 9.53/1.88 % (1241958)Instruction limit reached!
% 9.53/1.88 % (1241958)------------------------------
% 9.53/1.88 % (1241958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.53/1.88 % (1241958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.53/1.88 % (1241958)CaDiCaL version: 2.1.3
% 9.53/1.88 % (1241958)Termination reason: Instruction limit
% 9.53/1.88 % (1241958)Termination phase: Saturation
% 9.53/1.88 % (1241958)Time elapsed: 0.092 s
% 9.53/1.88 % (1241958)Peak memory usage: 12 MB
% 9.53/1.88 % (1241958)Instructions burned: 181 (million)
% 9.53/1.88 % (1241974)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3108720735:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 9.53/1.88 % (1241974)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 9.53/1.88 % (1241959)Instruction limit reached!
% 9.53/1.88 % (1241959)------------------------------
% 9.53/1.88 % (1241959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.53/1.88 % (1241959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.53/1.88 % (1241959)CaDiCaL version: 2.1.3
% 9.53/1.88 % (1241959)Termination reason: Instruction limit
% 9.53/1.88 % (1241959)Termination phase: Saturation
% 9.53/1.88 % (1241959)Time elapsed: 0.243 s
% 9.53/1.88 % (1241959)Peak memory usage: 13 MB
% 9.53/1.88 % (1241959)Instructions burned: 478 (million)
% 9.53/1.88 % (1241976)fmb+10_1_sil=64000:random_seed=144215818:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 9.53/1.88 % (1241976)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 9.53/1.88 % Exception at run slice level
% 9.53/1.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.53/1.88 % (1241978)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3046905052:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 9.53/1.88 % Exception at run slice level
% 9.53/1.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.53/1.88 % (1241980)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3285412265:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 9.53/1.88 % Exception at run slice level
% 9.53/1.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.53/1.88 % (1241982)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3291951470:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 9.53/1.88 % (1241982)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 9.53/1.88 % (1241972)Instruction limit reached!
% 9.53/1.88 % (1241972)------------------------------
% 9.53/1.88 % (1241972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.53/1.88 % (1241972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.53/1.88 % (1241972)CaDiCaL version: 2.1.3
% 9.53/1.88 % (1241972)Termination reason: Instruction limit
% 9.53/1.88 % (1241972)Termination phase: Saturation
% 9.53/1.88 % (1241972)Time elapsed: 0.292 s
% 9.53/1.88 % (1241972)Peak memory usage: 13 MB
% 9.53/1.88 % (1241972)Instructions burned: 692 (million)
% 9.53/1.88 % (1241985)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3024317576:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi)
% 9.53/1.88 % (1241985)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 9.53/1.88 % (1241985)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 9.53/1.88 % (1241957)Instruction limit reached!
% 9.53/1.88 % (1241957)------------------------------
% 9.53/1.88 % (1241957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.53/1.88 % (1241957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.53/1.88 % (1241957)CaDiCaL version: 2.1.3
% 9.53/1.88 % (1241957)Termination reason: Instruction limit
% 9.53/1.88 % (1241957)Termination phase: Saturation
% 9.53/1.88 % (1241957)Time elapsed: 0.492 s
% 9.53/1.88 % (1241957)Peak memory usage: 14 MB
% 9.53/1.88 % (1241957)Instructions burned: 685 (million)
% 9.53/1.88 % (1241990)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2505130792:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 9.53/1.88 % Exception at run slice level
% 9.53/1.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.53/1.88 % (1241992)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4167046320:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 9.53/1.88 % Exception at run slice level
% 9.53/1.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.53/1.88 % (1241994)ott-2_1_sil=16000:newcnf=on:random_seed=1837776141:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi)
% 9.53/1.88 % (1241994)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 9.53/1.88 % (1241968)Instruction limit reached!
% 9.53/1.88 % (1241968)------------------------------
% 9.53/1.88 % (1241968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.53/1.88 % (1241968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.53/1.88 % (1241968)CaDiCaL version: 2.1.3
% 9.53/1.88 % (1241968)Termination reason: Instruction limit
% 9.53/1.88 % (1241968)Termination phase: Saturation
% 9.53/1.88 % (1241968)Time elapsed: 0.564 s
% 9.53/1.88 % (1241968)Peak memory usage: 16 MB
% 9.53/1.88 % (1241968)Instructions burned: 1181 (million)
% 9.53/1.88 % (1241996)ott+10_1_sil=32000:tgt=ground:random_seed=1984625859:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 9.53/1.88 % (1241974)Instruction limit reached!
% 9.53/1.88 % (1241974)------------------------------
% 9.53/1.88 % (1241974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.53/1.88 % (1241974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.53/1.88 % (1241974)CaDiCaL version: 2.1.3
% 9.53/1.88 % (1241974)Termination reason: Instruction limit
% 9.53/1.88 % (1241974)Termination phase: Saturation
% 9.53/1.88 % (1241974)Time elapsed: 0.671 s
% 9.53/1.88 % (1241974)Peak memory usage: 16 MB
% 9.53/1.88 % (1241974)Instructions burned: 880 (million)
% 9.53/1.88 % (1241998)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1716311697:i=54282_2990 on theBenchmark for (2990ds/54282Mi)
% 9.53/1.88 % Exception at run slice level
% 9.53/1.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 9.53/1.88 % (1242000)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=257996560:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 9.53/1.88 % (1242000)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 9.53/1.88 % (1241994)Instruction limit reached!
% 9.53/1.88 % (1241994)------------------------------
% 9.53/1.88 % (1241994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.53/1.88 % (1241994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.53/1.88 % (1241994)CaDiCaL version: 2.1.3
% 9.53/1.88 % (1241994)Termination reason: Instruction limit
% 9.53/1.88 % (1241994)Termination phase: Saturation
% 9.53/1.88 % (1241994)Time elapsed: 0.414 s
% 9.53/1.88 % (1241994)Peak memory usage: 15 MB
% 9.53/1.88 % (1241994)Instructions burned: 870 (million)
% 9.53/1.88 % (1242002)dis+21_1_sil=32000:sas=cadical:random_seed=3751133679:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 9.53/1.88 % (1241985)Instruction limit reached!
% 9.53/1.88 % (1241985)------------------------------
% 9.53/1.88 % (1241985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.53/1.88 % (1241985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.53/1.88 % (1241985)CaDiCaL version: 2.1.3
% 9.53/1.88 % (1241985)Termination reason: Instruction limit
% 9.53/1.88 % (1241985)Termination phase: Saturation
% 9.53/1.88 % (1241985)Time elapsed: 0.739 s
% 9.53/1.88 % (1241985)Peak memory usage: 19 MB
% 9.53/1.88 % (1241985)Instructions burned: 1473 (million)
% 9.53/1.88 % (1242004)ott+11_1_sil=16000:gs=on:random_seed=4218358690:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 9.53/1.88 % (1242004)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 9.53/1.88 % (1242002) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1241933-1242002"...
% 9.53/1.88 % (1242002)...printing done.
% 9.53/1.88 % (1242002)Refutation found. Thanks to Tanya!
% 9.53/1.88 % SZS status Theorem for theBenchmark
% 9.53/1.88 % SZS output start Proof for theBenchmark
% 9.53/1.88 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 9.53/1.88 thf(func_def_0, type, cN: ($i > $o)).
% 9.53/1.88 thf(func_def_1, type, cODD: ($i > $o)).
% 9.53/1.88 thf(func_def_2, type, cEVEN: ($i > $o)).
% 9.53/1.88 thf(func_def_3, type, cS: ($i > $i)).
% 9.53/1.88 thf(func_def_9, type, sK1: (($i > $o) > ($i > $o) > $i)).
% 9.53/1.88 thf(func_def_10, type, sK2: (($i > $o) > ($i > $o) > $i)).
% 9.53/1.88 thf(func_def_11, type, vNOT: ($o > $o)).
% 9.53/1.88 thf(func_def_13, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 9.53/1.88 thf(func_def_14, type, db0: !>[X0: $tType]:(X0)).
% 9.53/1.88 thf(func_def_15, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 9.53/1.88 thf(func_def_16, type, db1: !>[X0: $tType]:(X0)).
% 9.53/1.88 thf(f1,conjecture,(
% 9.53/1.88 (! [X5 : $i] : ((cN @ X5) => (cN @ (cS @ X5))) & (cN @ c0) & ! [X0 : ($i > $o),X1 : ($i > $o)] : ((! [X3 : $i] : ((X1 @ X3) => (X0 @ (cS @ X3))) & ! [X2 : $i] : ((X0 @ X2) => (X1 @ (cS @ X2))) & (X0 @ c0)) => (! [X4 : $i] : ((cODD @ X4) => (X1 @ X4)) & ! [X4 : $i] : ((cEVEN @ X4) => (X0 @ X4))))) => ! [X6 : $i] : (((cODD @ X6) | (cEVEN @ X6)) => (cN @ X6))),
% 9.53/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM623_pme)).
% 9.53/1.88 thf(f2,negated_conjecture,(
% 9.53/1.88 ~((! [X5 : $i] : ((cN @ X5) => (cN @ (cS @ X5))) & (cN @ c0) & ! [X0 : ($i > $o),X1 : ($i > $o)] : ((! [X3 : $i] : ((X1 @ X3) => (X0 @ (cS @ X3))) & ! [X2 : $i] : ((X0 @ X2) => (X1 @ (cS @ X2))) & (X0 @ c0)) => (! [X4 : $i] : ((cODD @ X4) => (X1 @ X4)) & ! [X4 : $i] : ((cEVEN @ X4) => (X0 @ X4))))) => ! [X6 : $i] : (((cODD @ X6) | (cEVEN @ X6)) => (cN @ X6)))),
% 9.53/1.88 inference(negated_conjecture,[status(cth)],[f1])).
% 9.53/1.88 thf(f3,plain,(
% 9.53/1.88 ~((! [X0 : $i] : ((cN @ X0) => (cN @ (cS @ X0))) & (cN @ c0) & ! [X1 : ($i > $o),X2 : ($i > $o)] : ((! [X3 : $i] : ((X2 @ X3) => (X1 @ (cS @ X3))) & ! [X4 : $i] : ((X1 @ X4) => (X2 @ (cS @ X4))) & (X1 @ c0)) => (! [X5 : $i] : ((cODD @ X5) => (X2 @ X5)) & ! [X6 : $i] : ((cEVEN @ X6) => (X1 @ X6))))) => ! [X7 : $i] : (((cODD @ X7) | (cEVEN @ X7)) => (cN @ X7)))),
% 9.53/1.88 inference(rectify,[],[f2])).
% 9.53/1.88 thf(f4,plain,(
% 9.53/1.88 ~((! [X0 : $i] : ((((cN @ X0)) = $true) => (((cN @ (cS @ X0))) = $true)) & (((cN @ c0)) = $true) & ! [X1 : ($i > $o),X2 : ($i > $o)] : ((! [X3 : $i] : ((((X2 @ X3)) = $true) => (((X1 @ (cS @ X3))) = $true)) & ! [X4 : $i] : ((((X1 @ X4)) = $true) => (((X2 @ (cS @ X4))) = $true)) & (((X1 @ c0)) = $true)) => (! [X5 : $i] : ((((cODD @ X5)) = $true) => (((X2 @ X5)) = $true)) & ! [X6 : $i] : ((((cEVEN @ X6)) = $true) => (((X1 @ X6)) = $true))))) => ! [X7 : $i] : (((((cODD @ X7)) = $true) | (((cEVEN @ X7)) = $true)) => (((cN @ X7)) = $true)))),
% 9.53/1.88 inference(fool_elimination,[],[f3])).
% 9.53/1.88 thf(f5,plain,(
% 9.53/1.88 ? [X7 : $i] : ((((cN @ X7)) != $true) & ((((cODD @ X7)) = $true) | (((cEVEN @ X7)) = $true))) & (! [X0 : $i] : ((((cN @ (cS @ X0))) = $true) | (((cN @ X0)) != $true)) & (((cN @ c0)) = $true) & ! [X1 : ($i > $o),X2 : ($i > $o)] : ((! [X5 : $i] : ((((X2 @ X5)) = $true) | (((cODD @ X5)) != $true)) & ! [X6 : $i] : ((((X1 @ X6)) = $true) | (((cEVEN @ X6)) != $true))) | (? [X3 : $i] : ((((X1 @ (cS @ X3))) != $true) & (((X2 @ X3)) = $true)) | ? [X4 : $i] : ((((X2 @ (cS @ X4))) != $true) & (((X1 @ X4)) = $true)) | (((X1 @ c0)) != $true))))),
% 9.53/1.88 inference(ennf_transformation,[],[f4])).
% 9.53/1.88 thf(f6,plain,(
% 9.53/1.88 ? [X7 : $i] : ((((cN @ X7)) != $true) & ((((cODD @ X7)) = $true) | (((cEVEN @ X7)) = $true))) & ! [X0 : $i] : ((((cN @ (cS @ X0))) = $true) | (((cN @ X0)) != $true)) & (((cN @ c0)) = $true) & ! [X1 : ($i > $o),X2 : ($i > $o)] : ((! [X5 : $i] : ((((X2 @ X5)) = $true) | (((cODD @ X5)) != $true)) & ! [X6 : $i] : ((((X1 @ X6)) = $true) | (((cEVEN @ X6)) != $true))) | ? [X3 : $i] : ((((X1 @ (cS @ X3))) != $true) & (((X2 @ X3)) = $true)) | ? [X4 : $i] : ((((X2 @ (cS @ X4))) != $true) & (((X1 @ X4)) = $true)) | (((X1 @ c0)) != $true))),
% 9.53/1.88 inference(flattening,[],[f5])).
% 9.53/1.88 thf(f7,plain,(
% 9.53/1.88 ? [X0 : $i] : ((((cN @ X0)) != $true) & (($true = ((cODD @ X0))) | ($true = ((cEVEN @ X0))))) & ! [X1 : $i] : (($true = ((cN @ (cS @ X1)))) | ($true != ((cN @ X1)))) & (((cN @ c0)) = $true) & ! [X2 : ($i > $o),X3 : ($i > $o)] : ((! [X4 : $i] : (($true = ((X3 @ X4))) | (((cODD @ X4)) != $true)) & ! [X5 : $i] : ((((X2 @ X5)) = $true) | ($true != ((cEVEN @ X5))))) | ? [X6 : $i] : (($true != ((X2 @ (cS @ X6)))) & ($true = ((X3 @ X6)))) | ? [X7 : $i] : (($true != ((X3 @ (cS @ X7)))) & ($true = ((X2 @ X7)))) | ($true != ((X2 @ c0))))),
% 9.53/1.88 inference(rectify,[],[f6])).
% 9.53/1.88 thf(f8,plain,(
% 9.53/1.88 (($true != ((cN @ sK0))) & (($true = ((cODD @ sK0))) | ($true = ((cEVEN @ sK0))))) & ! [X1 : $i] : (($true = ((cN @ (cS @ X1)))) | ($true != ((cN @ X1)))) & (((cN @ c0)) = $true) & ! [X2 : ($i > $o),X3 : ($i > $o)] : ((! [X4 : $i] : (($true = ((X3 @ X4))) | (((cODD @ X4)) != $true)) & ! [X5 : $i] : ((((X2 @ X5)) = $true) | ($true != ((cEVEN @ X5))))) | (($true != ((X2 @ (cS @ (sK1 @ X3 @ X2))))) & ($true = ((X3 @ (sK1 @ X3 @ X2))))) | (($true != ((X3 @ (cS @ (sK2 @ X3 @ X2))))) & ($true = ((X2 @ (sK2 @ X3 @ X2))))) | ($true != ((X2 @ c0))))),
% 9.53/1.88 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,vAPP,vAPP]),skolemize(X0,sK0),skolemize(X7,sK2 @ X3 @ X2),skolemize(X7,sK2 @ X3 @ X2)],[f7])).
% 9.53/1.88 thf(f9,plain,(
% 9.53/1.88 ( ! [X2 : ($i > $o),X3 : ($i > $o),X5 : $i] : (($true != ((X2 @ c0))) | ($true != ((cEVEN @ X5))) | ($true = ((X3 @ (sK1 @ X3 @ X2)))) | ($true = ((X2 @ (sK2 @ X3 @ X2)))) | (((X2 @ X5)) = $true)) )),
% 9.53/1.88 inference(cnf_transformation,[],[f8])).
% 9.53/1.88 thf(f10,plain,(
% 9.53/1.88 ( ! [X2 : ($i > $o),X3 : ($i > $o),X5 : $i] : (($true != ((X3 @ (cS @ (sK2 @ X3 @ X2))))) | ($true != ((cEVEN @ X5))) | ($true = ((X3 @ (sK1 @ X3 @ X2)))) | (((X2 @ X5)) = $true) | ($true != ((X2 @ c0)))) )),
% 9.53/1.88 inference(cnf_transformation,[],[f8])).
% 9.53/1.88 thf(f11,plain,(
% 9.53/1.88 ( ! [X2 : ($i > $o),X3 : ($i > $o),X5 : $i] : (($true != ((X2 @ (cS @ (sK1 @ X3 @ X2))))) | ($true != ((cEVEN @ X5))) | (((X2 @ X5)) = $true) | ($true = ((X2 @ (sK2 @ X3 @ X2)))) | ($true != ((X2 @ c0)))) )),
% 9.53/1.88 inference(cnf_transformation,[],[f8])).
% 9.53/1.88 thf(f12,plain,(
% 9.53/1.88 ( ! [X2 : ($i > $o),X3 : ($i > $o),X5 : $i] : (($true != ((X3 @ (cS @ (sK2 @ X3 @ X2))))) | ($true != ((cEVEN @ X5))) | ($true != ((X2 @ (cS @ (sK1 @ X3 @ X2))))) | (((X2 @ X5)) = $true) | ($true != ((X2 @ c0)))) )),
% 9.53/1.88 inference(cnf_transformation,[],[f8])).
% 9.53/1.88 thf(f13,plain,(
% 9.53/1.88 ( ! [X2 : ($i > $o),X3 : ($i > $o),X4 : $i] : (($true != ((X2 @ c0))) | (((cODD @ X4)) != $true) | ($true = ((X3 @ (sK1 @ X3 @ X2)))) | ($true = ((X2 @ (sK2 @ X3 @ X2)))) | ($true = ((X3 @ X4)))) )),
% 9.53/1.88 inference(cnf_transformation,[],[f8])).
% 9.53/1.88 thf(f14,plain,(
% 9.53/1.88 ( ! [X2 : ($i > $o),X3 : ($i > $o),X4 : $i] : (($true != ((X3 @ (cS @ (sK2 @ X3 @ X2))))) | (((cODD @ X4)) != $true) | ($true = ((X3 @ (sK1 @ X3 @ X2)))) | ($true = ((X3 @ X4))) | ($true != ((X2 @ c0)))) )),
% 9.53/1.88 inference(cnf_transformation,[],[f8])).
% 9.53/1.88 thf(f15,plain,(
% 9.53/1.88 ( ! [X2 : ($i > $o),X3 : ($i > $o),X4 : $i] : (($true != ((X2 @ (cS @ (sK1 @ X3 @ X2))))) | (((cODD @ X4)) != $true) | ($true = ((X3 @ X4))) | ($true = ((X2 @ (sK2 @ X3 @ X2)))) | ($true != ((X2 @ c0)))) )),
% 9.53/1.88 inference(cnf_transformation,[],[f8])).
% 9.53/1.88 thf(f16,plain,(
% 9.53/1.88 ( ! [X2 : ($i > $o),X3 : ($i > $o),X4 : $i] : (($true != ((X3 @ (cS @ (sK2 @ X3 @ X2))))) | (((cODD @ X4)) != $true) | ($true != ((X2 @ (cS @ (sK1 @ X3 @ X2))))) | ($true = ((X3 @ X4))) | ($true != ((X2 @ c0)))) )),
% 9.53/1.88 inference(cnf_transformation,[],[f8])).
% 9.53/1.88 thf(f17,plain,(
% 9.53/1.88 (((cN @ c0)) = $true)),
% 9.53/1.88 inference(cnf_transformation,[],[f8])).
% 9.53/1.88 thf(f18,plain,(
% 9.53/1.88 ( ! [X1 : $i] : (($true = ((cN @ (cS @ X1)))) | ($true != ((cN @ X1)))) )),
% 9.53/1.88 inference(cnf_transformation,[],[f8])).
% 9.53/1.88 thf(f19,plain,(
% 9.53/1.88 ($true = ((cODD @ sK0))) | ($true = ((cEVEN @ sK0)))),
% 9.53/1.88 inference(cnf_transformation,[],[f8])).
% 9.53/1.88 thf(f20,plain,(
% 9.53/1.88 ($true != ((cN @ sK0)))),
% 9.53/1.88 inference(cnf_transformation,[],[f8])).
% 9.53/1.88 thf(f22,definition,(
% 9.53/1.88 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 9.53/1.88 introduced(theory,[fool_exhaustiveness_axiom])).
% 9.53/1.88 thf(f24,definition,(
% 9.53/1.88 spl3_1 <=> ($true = ((cEVEN @ sK0)))),
% 9.53/1.88 introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition])).
% 9.53/1.88 thf(f28,definition,(
% 9.53/1.88 spl3_2 <=> ($true = ((cODD @ sK0)))),
% 9.53/1.88 introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition])).
% 9.53/1.88 thf(f30,plain,(
% 9.53/1.88 ($true = ((cODD @ sK0))) | ~spl3_2),
% 9.53/1.88 inference(avatar_component_clause,[],[f28])).
% 9.53/1.88 thf(f31,plain,(
% 9.53/1.88 spl3_1 | spl3_2),
% 9.53/1.88 inference(avatar_split_clause,[],[f19,f28,f24])).
% 9.53/1.88 thf(f34,plain,(
% 9.53/1.88 ($true != $true) | (((cN @ sK0)) = $false)),
% 9.53/1.88 inference(constrained_superposition,[],[f20,f22])).
% 9.53/1.88 thf(f36,plain,(
% 9.53/1.88 (((cN @ sK0)) = $false)),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f34])).
% 9.53/1.88 thf(f45,plain,(
% 9.53/1.88 ( ! [X0 : $i,X1 : ($i > $o)] : (($true != $true) | ($true != ((cEVEN @ X0))) | ($true = ((X1 @ (sK1 @ X1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK2 @ X1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0)))) )),
% 9.53/1.88 inference(constrained_superposition,[],[f9,f17])).
% 9.53/1.88 thf(f69,plain,(
% 9.53/1.88 ( ! [X0 : $i,X1 : ($i > $o)] : (($true != ((cEVEN @ X0))) | ($true = ((X1 @ (sK1 @ X1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK2 @ X1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0)))) )),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f45])).
% 9.53/1.88 thf(f70,plain,(
% 9.53/1.88 ( ! [X0 : $i,X1 : ($i > $o)] : (($true != ((cEVEN @ X0))) | ($true = ((X1 @ (sK1 @ X1 @ cN)))) | ($true = ((cN @ (sK2 @ X1 @ cN)))) | (((cN @ X0)) = $true)) )),
% 9.53/1.88 inference(beta-eta_normalization,[],[f69])).
% 9.53/1.88 thf(f81,definition,(
% 9.53/1.88 spl3_3 <=> ! [X1 : ($i > $o)] : (($true = ((X1 @ (sK1 @ X1 @ cN)))) | ($true = ((cN @ (sK2 @ X1 @ cN)))))),
% 9.53/1.88 introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition])).
% 9.53/1.88 thf(f82,plain,(
% 9.53/1.88 ( ! [X1 : ($i > $o)] : (($true = ((X1 @ (sK1 @ X1 @ cN)))) | ($true = ((cN @ (sK2 @ X1 @ cN))))) ) | ~spl3_3),
% 9.53/1.88 inference(avatar_component_clause,[],[f81])).
% 9.53/1.88 thf(f84,definition,(
% 9.53/1.88 spl3_4 <=> ! [X0 : $i] : (($true != ((cEVEN @ X0))) | (((cN @ X0)) = $true))),
% 9.53/1.88 introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition])).
% 9.53/1.88 thf(f85,plain,(
% 9.53/1.88 ( ! [X0 : $i] : ((((cN @ X0)) = $true) | ($true != ((cEVEN @ X0)))) ) | ~spl3_4),
% 9.53/1.88 inference(avatar_component_clause,[],[f84])).
% 9.53/1.88 thf(f86,plain,(
% 9.53/1.88 spl3_3 | spl3_4),
% 9.53/1.88 inference(avatar_split_clause,[],[f70,f84,f81])).
% 9.53/1.88 thf(f104,plain,(
% 9.53/1.88 ( ! [X0 : $i,X1 : ($i > $o)] : (($true != $true) | ($true != ((cODD @ X0))) | ($true = ((X1 @ (sK1 @ X1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK2 @ X1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($true = ((X1 @ X0)))) )),
% 9.53/1.88 inference(constrained_superposition,[],[f13,f17])).
% 9.53/1.88 thf(f125,plain,(
% 9.53/1.88 ( ! [X0 : $i,X1 : ($i > $o)] : (($true != ((cODD @ X0))) | ($true = ((X1 @ (sK1 @ X1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK2 @ X1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($true = ((X1 @ X0)))) )),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f104])).
% 9.53/1.88 thf(f126,plain,(
% 9.53/1.88 ( ! [X0 : $i,X1 : ($i > $o)] : (($true != ((cODD @ X0))) | ($true = ((X1 @ (sK1 @ X1 @ cN)))) | ($true = ((cN @ (sK2 @ X1 @ cN)))) | ($true = ((X1 @ X0)))) )),
% 9.53/1.88 inference(beta-eta_normalization,[],[f125])).
% 9.53/1.88 thf(f140,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != $true) | ($true != ((cEVEN @ X2))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0)))) | (((X0 @ X2)) = $true) | (((X0 @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK2 @ cN @ X0)) != X1)) )),
% 9.53/1.88 inference(constrained_superposition,[],[f10,f18])).
% 9.53/1.88 thf(f158,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((cEVEN @ X2))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0)))) | (((X0 @ X2)) = $true) | (((X0 @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK2 @ cN @ X0)) != X1)) )),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f140])).
% 9.53/1.88 thf(f159,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : ((((sK2 @ cN @ X0)) != X1) | ($true = ((cN @ (sK1 @ cN @ X0)))) | (((X0 @ X2)) = $true) | (((X0 @ c0)) != $true) | ($true != ((cN @ X1))) | ($true != ((cEVEN @ X2)))) )),
% 9.53/1.88 inference(beta-eta_normalization,[],[f158])).
% 9.53/1.88 thf(f178,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != $true) | ($true != ((cEVEN @ X2))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X2))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK2 @ X0 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($true != (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ c0))) | ($true != ((cN @ X1))) | (((sK1 @ X0 @ cN)) != X1)) )),
% 9.53/1.88 inference(constrained_superposition,[],[f11,f18])).
% 9.53/1.88 thf(f201,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((cEVEN @ X2))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X2))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK2 @ X0 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($true != (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ c0))) | ($true != ((cN @ X1))) | (((sK1 @ X0 @ cN)) != X1)) )),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f178])).
% 9.53/1.88 thf(f202,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((cEVEN @ X2))) | ($true = ((cN @ X2))) | ($true = ((cN @ (sK2 @ X0 @ cN)))) | (((cN @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK1 @ X0 @ cN)) != X1)) )),
% 9.53/1.88 inference(beta-eta_normalization,[],[f201])).
% 9.53/1.88 thf(f220,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((cEVEN @ X2))) | ($true = ((cN @ X2))) | ($true = ((cN @ (sK2 @ X0 @ cN)))) | ($true != ((cN @ X1))) | (((sK1 @ X0 @ cN)) != X1)) )),
% 9.53/1.88 inference(forward_subsumption_resolution,[],[f202,f17])).
% 9.53/1.88 thf(f222,definition,(
% 9.53/1.88 spl3_7 <=> ! [X0 : ($i > $o),X1 : $i] : (($true = ((cN @ (sK2 @ X0 @ cN)))) | (((sK1 @ X0 @ cN)) != X1) | ($true != ((cN @ X1))))),
% 9.53/1.88 introduced(definition,[new_symbols(definition,[spl3_7])],[avatar_definition])).
% 9.53/1.88 thf(f223,plain,(
% 9.53/1.88 ( ! [X0 : ($i > $o),X1 : $i] : ((((sK1 @ X0 @ cN)) != X1) | ($true = ((cN @ (sK2 @ X0 @ cN)))) | ($true != ((cN @ X1)))) ) | ~spl3_7),
% 9.53/1.88 inference(avatar_component_clause,[],[f222])).
% 9.53/1.88 thf(f224,plain,(
% 9.53/1.88 spl3_7 | spl3_4),
% 9.53/1.88 inference(avatar_split_clause,[],[f220,f84,f222])).
% 9.53/1.88 thf(f225,plain,(
% 9.53/1.88 ($true = $false) | ($true != ((cEVEN @ sK0))) | ~spl3_4),
% 9.53/1.88 inference(constrained_superposition,[],[f85,f36])).
% 9.53/1.88 thf(f253,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != $true) | ($true != ((cODD @ X2))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0)))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X2))) | (((X0 @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK2 @ cN @ X0)) != X1)) )),
% 9.53/1.88 inference(constrained_superposition,[],[f14,f18])).
% 9.53/1.88 thf(f276,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((cODD @ X2))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0)))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X2))) | (((X0 @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK2 @ cN @ X0)) != X1)) )),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f253])).
% 9.53/1.88 thf(f277,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((cODD @ X2))) | ($true = ((cN @ (sK1 @ cN @ X0)))) | ($true = ((cN @ X2))) | (((X0 @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK2 @ cN @ X0)) != X1)) )),
% 9.53/1.88 inference(beta-eta_normalization,[],[f276])).
% 9.53/1.88 thf(f290,definition,(
% 9.53/1.88 spl3_8 <=> ! [X0 : ($i > $o),X1 : $i] : (($true = ((cN @ (sK1 @ cN @ X0)))) | (((sK2 @ cN @ X0)) != X1) | ($true != ((cN @ X1))) | (((X0 @ c0)) != $true))),
% 9.53/1.88 introduced(definition,[new_symbols(definition,[spl3_8])],[avatar_definition])).
% 9.53/1.88 thf(f291,plain,(
% 9.53/1.88 ( ! [X0 : ($i > $o),X1 : $i] : ((((sK2 @ cN @ X0)) != X1) | ($true = ((cN @ (sK1 @ cN @ X0)))) | ($true != ((cN @ X1))) | (((X0 @ c0)) != $true)) ) | ~spl3_8),
% 9.53/1.88 inference(avatar_component_clause,[],[f290])).
% 9.53/1.88 thf(f293,definition,(
% 9.53/1.88 spl3_9 <=> ! [X2 : $i] : (($true != ((cODD @ X2))) | ($true = ((cN @ X2))))),
% 9.53/1.88 introduced(definition,[new_symbols(definition,[spl3_9])],[avatar_definition])).
% 9.53/1.88 thf(f294,plain,(
% 9.53/1.88 ( ! [X2 : $i] : (($true = ((cN @ X2))) | ($true != ((cODD @ X2)))) ) | ~spl3_9),
% 9.53/1.88 inference(avatar_component_clause,[],[f293])).
% 9.53/1.88 thf(f295,plain,(
% 9.53/1.88 spl3_8 | spl3_9),
% 9.53/1.88 inference(avatar_split_clause,[],[f277,f293,f290])).
% 9.53/1.88 thf(f296,plain,(
% 9.53/1.88 ($true = $false) | ($true != ((cODD @ sK0))) | ~spl3_9),
% 9.53/1.88 inference(constrained_superposition,[],[f294,f36])).
% 9.53/1.88 thf(f327,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != $true) | ($true != ((cODD @ X2))) | (((X0 @ X2)) = $true) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK2 @ X0 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($true != (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ c0))) | ($true != ((cN @ X1))) | (((sK1 @ X0 @ cN)) != X1)) )),
% 9.53/1.88 inference(constrained_superposition,[],[f15,f18])).
% 9.53/1.88 thf(f345,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((cODD @ X2))) | (((X0 @ X2)) = $true) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK2 @ X0 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | ($true != (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ c0))) | ($true != ((cN @ X1))) | (((sK1 @ X0 @ cN)) != X1)) )),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f327])).
% 9.53/1.88 thf(f346,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((cODD @ X2))) | (((X0 @ X2)) = $true) | ($true = ((cN @ (sK2 @ X0 @ cN)))) | (((cN @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK1 @ X0 @ cN)) != X1)) )),
% 9.53/1.88 inference(beta-eta_normalization,[],[f345])).
% 9.53/1.88 thf(f357,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : ((((sK1 @ X0 @ cN)) != X1) | (((X0 @ X2)) = $true) | ($true = ((cN @ (sK2 @ X0 @ cN)))) | ($true != ((cN @ X1))) | ($true != ((cODD @ X2)))) )),
% 9.53/1.88 inference(forward_subsumption_resolution,[],[f346,f17])).
% 9.53/1.88 thf(f476,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != $true) | ($true != ((cEVEN @ X2))) | ($true != ((X0 @ (cS @ (sK1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0))))) | (((X0 @ X2)) = $true) | (((X0 @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK2 @ cN @ X0)) != X1)) )),
% 9.53/1.88 inference(constrained_superposition,[],[f12,f18])).
% 9.53/1.88 thf(f495,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((cEVEN @ X2))) | ($true != ((X0 @ (cS @ (sK1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0))))) | (((X0 @ X2)) = $true) | (((X0 @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK2 @ cN @ X0)) != X1)) )),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f476])).
% 9.53/1.88 thf(f496,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((X0 @ (cS @ (sK1 @ cN @ X0))))) | ($true != ((cEVEN @ X2))) | (((X0 @ X2)) = $true) | (((X0 @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK2 @ cN @ X0)) != X1)) )),
% 9.53/1.88 inference(beta-eta_normalization,[],[f495])).
% 9.53/1.88 thf(f608,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != $true) | ($true != ((cODD @ X2))) | ($true != ((X0 @ (cS @ (sK1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0))))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X2))) | (((X0 @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK2 @ cN @ X0)) != X1)) )),
% 9.53/1.88 inference(constrained_superposition,[],[f16,f18])).
% 9.53/1.88 thf(f627,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((cODD @ X2))) | ($true != ((X0 @ (cS @ (sK1 @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0))))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X2))) | (((X0 @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK2 @ cN @ X0)) != X1)) )),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f608])).
% 9.53/1.88 thf(f628,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : ($i > $o),X1 : $i] : (($true != ((cODD @ X2))) | ($true != ((X0 @ (cS @ (sK1 @ cN @ X0))))) | ($true = ((cN @ X2))) | (((X0 @ c0)) != $true) | ($true != ((cN @ X1))) | (((sK2 @ cN @ X0)) != X1)) )),
% 9.53/1.88 inference(beta-eta_normalization,[],[f627])).
% 9.53/1.88 thf(f642,definition,(
% 9.53/1.88 spl3_20 <=> ! [X0 : ($i > $o),X1 : $i] : (($true != ((X0 @ (cS @ (sK1 @ cN @ X0))))) | (((sK2 @ cN @ X0)) != X1) | ($true != ((cN @ X1))) | (((X0 @ c0)) != $true))),
% 9.53/1.88 introduced(definition,[new_symbols(definition,[spl3_20])],[avatar_definition])).
% 9.53/1.88 thf(f643,plain,(
% 9.53/1.88 ( ! [X0 : ($i > $o),X1 : $i] : (($true != ((X0 @ (cS @ (sK1 @ cN @ X0))))) | (((sK2 @ cN @ X0)) != X1) | ($true != ((cN @ X1))) | (((X0 @ c0)) != $true)) ) | ~spl3_20),
% 9.53/1.88 inference(avatar_component_clause,[],[f642])).
% 9.53/1.88 thf(f644,plain,(
% 9.53/1.88 spl3_20 | spl3_9),
% 9.53/1.88 inference(avatar_split_clause,[],[f628,f293,f642])).
% 9.53/1.88 thf(f675,plain,(
% 9.53/1.88 ( ! [X0 : ($i > $o)] : (($true = ((cN @ (sK2 @ X0 @ cN)))) | ($true != ((cN @ (sK1 @ X0 @ cN))))) ) | ~spl3_7),
% 9.53/1.88 inference(equality_resolution,[],[f223])).
% 9.53/1.88 thf(f1120,plain,(
% 9.53/1.88 ( ! [X0 : ($i > $o)] : (($true != ((cN @ (sK2 @ cN @ X0)))) | ($true = ((cN @ (sK1 @ cN @ X0)))) | (((X0 @ c0)) != $true)) ) | ~spl3_8),
% 9.53/1.88 inference(equality_resolution,[],[f291])).
% 9.53/1.88 thf(f1175,plain,(
% 9.53/1.88 ( ! [X0 : $i,X1 : $i] : (($true != $true) | (((sK2 @ cN @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))) != X1) | ($true != ((cN @ X1))) | ($true != (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ c0))) | (((cN @ X0)) != $true) | (((sK1 @ cN @ cN)) != X0)) ) | ~spl3_20),
% 9.53/1.88 inference(constrained_superposition,[],[f643,f18])).
% 9.53/1.88 thf(f1206,plain,(
% 9.53/1.88 ( ! [X0 : $i,X1 : $i] : ((((sK2 @ cN @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))) != X1) | ($true != ((cN @ X1))) | ($true != (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ c0))) | (((cN @ X0)) != $true) | (((sK1 @ cN @ cN)) != X0)) ) | ~spl3_20),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f1175])).
% 9.53/1.88 thf(f1207,plain,(
% 9.53/1.88 ( ! [X0 : $i,X1 : $i] : ((((sK2 @ cN @ cN)) != X1) | ($true != ((cN @ X1))) | (((cN @ c0)) != $true) | (((cN @ X0)) != $true) | (((sK1 @ cN @ cN)) != X0)) ) | ~spl3_20),
% 9.53/1.88 inference(beta-eta_normalization,[],[f1206])).
% 9.53/1.88 thf(f1230,plain,(
% 9.53/1.88 ( ! [X0 : $i,X1 : $i] : ((((sK2 @ cN @ cN)) != X1) | ($true != ((cN @ X1))) | (((cN @ X0)) != $true) | (((sK1 @ cN @ cN)) != X0)) ) | ~spl3_20),
% 9.53/1.88 inference(forward_subsumption_resolution,[],[f1207,f17])).
% 9.53/1.88 thf(f1245,definition,(
% 9.53/1.88 spl3_33 <=> ! [X0 : $i] : ((((cN @ X0)) != $true) | (((sK1 @ cN @ cN)) != X0))),
% 9.53/1.88 introduced(definition,[new_symbols(definition,[spl3_33])],[avatar_definition])).
% 9.53/1.88 thf(f1246,plain,(
% 9.53/1.88 ( ! [X0 : $i] : ((((sK1 @ cN @ cN)) != X0) | (((cN @ X0)) != $true)) ) | ~spl3_33),
% 9.53/1.88 inference(avatar_component_clause,[],[f1245])).
% 9.53/1.88 thf(f1248,definition,(
% 9.53/1.88 spl3_34 <=> ! [X1 : $i] : ((((sK2 @ cN @ cN)) != X1) | ($true != ((cN @ X1))))),
% 9.53/1.88 introduced(definition,[new_symbols(definition,[spl3_34])],[avatar_definition])).
% 9.53/1.88 thf(f1249,plain,(
% 9.53/1.88 ( ! [X1 : $i] : ((((sK2 @ cN @ cN)) != X1) | ($true != ((cN @ X1)))) ) | ~spl3_34),
% 9.53/1.88 inference(avatar_component_clause,[],[f1248])).
% 9.53/1.88 thf(f1250,plain,(
% 9.53/1.88 spl3_33 | spl3_34 | ~spl3_20),
% 9.53/1.88 inference(avatar_split_clause,[],[f1230,f642,f1248,f1245])).
% 9.53/1.88 thf(f1251,plain,(
% 9.53/1.88 ($true != ((cN @ (sK1 @ cN @ cN)))) | ~spl3_33),
% 9.53/1.88 inference(equality_resolution,[],[f1246])).
% 9.53/1.88 thf(f1351,plain,(
% 9.53/1.88 ($true != ((cN @ (sK2 @ cN @ cN)))) | ~spl3_34),
% 9.53/1.88 inference(equality_resolution,[],[f1249])).
% 9.53/1.88 thf(f3195,plain,(
% 9.53/1.88 ($true != $true) | ($true != ((cN @ (sK1 @ cN @ cN)))) | (~spl3_7 | ~spl3_34)),
% 9.53/1.88 inference(constrained_superposition,[],[f1351,f675])).
% 9.53/1.88 thf(f3280,plain,(
% 9.53/1.88 ($true != ((cEVEN @ sK0))) | ~spl3_4),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f225])).
% 9.53/1.88 thf(f3283,plain,(
% 9.53/1.88 ~spl3_1 | ~spl3_4),
% 9.53/1.88 inference(avatar_split_clause,[],[f3280,f84,f24])).
% 9.53/1.88 thf(f3461,plain,(
% 9.53/1.88 ( ! [X0 : ($i > $o)] : (($true != $true) | ($true = ((X0 @ (sK1 @ X0 @ cN)))) | ($true = ((cN @ (sK2 @ X0 @ cN)))) | ($true = ((X0 @ sK0)))) ) | ~spl3_2),
% 9.53/1.88 inference(constrained_superposition,[],[f126,f30])).
% 9.53/1.88 thf(f3462,plain,(
% 9.53/1.88 ( ! [X0 : ($i > $o)] : (($true = ((X0 @ (sK1 @ X0 @ cN)))) | ($true = ((cN @ (sK2 @ X0 @ cN)))) | ($true = ((X0 @ sK0)))) ) | ~spl3_2),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f3461])).
% 9.53/1.88 thf(f3547,plain,(
% 9.53/1.88 ( ! [X0 : ($i > $o),X1 : $i] : (($true != ((cN @ (sK1 @ X0 @ cN)))) | ($true = ((cN @ (sK2 @ X0 @ cN)))) | ($true = ((X0 @ X1))) | ($true != ((cODD @ X1)))) )),
% 9.53/1.88 inference(equality_resolution,[],[f357])).
% 9.53/1.88 thf(f3848,plain,(
% 9.53/1.88 ($true != $true) | ($true = ((cN @ (sK1 @ cN @ cN)))) | (((cN @ c0)) != $true) | ($true = ((cN @ (sK1 @ cN @ cN)))) | ($true = ((cN @ sK0))) | (~spl3_2 | ~spl3_8)),
% 9.53/1.88 inference(constrained_superposition,[],[f1120,f3462])).
% 9.53/1.88 thf(f3875,plain,(
% 9.53/1.88 ($true != $true) | ($true = ((cN @ (sK1 @ cN @ cN)))) | (((cN @ c0)) != $true) | ($true = ((cN @ sK0))) | (~spl3_2 | ~spl3_8)),
% 9.53/1.88 inference(duplicate_literal_removal,[],[f3848])).
% 9.53/1.88 thf(f3876,plain,(
% 9.53/1.88 ($true = ((cN @ (sK1 @ cN @ cN)))) | (((cN @ c0)) != $true) | ($true = ((cN @ sK0))) | (~spl3_2 | ~spl3_8)),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f3875])).
% 9.53/1.88 thf(f4075,plain,(
% 9.53/1.88 ($true = ((cN @ (sK1 @ cN @ cN)))) | ($true = ((cN @ sK0))) | (~spl3_2 | ~spl3_8)),
% 9.53/1.88 inference(forward_subsumption_resolution,[],[f3876,f17])).
% 9.53/1.88 thf(f4124,plain,(
% 9.53/1.88 ($true = ((cN @ (sK1 @ cN @ cN)))) | (~spl3_2 | ~spl3_8)),
% 9.53/1.88 inference(forward_subsumption_resolution,[],[f4075,f20])).
% 9.53/1.88 thf(f5648,plain,(
% 9.53/1.88 ( ! [X0 : $i] : (($true != $true) | ($true = ((cN @ (sK2 @ cN @ cN)))) | (((cN @ X0)) = $true) | ($true != ((cODD @ X0)))) ) | (~spl3_2 | ~spl3_8)),
% 9.53/1.88 inference(constrained_superposition,[],[f3547,f4124])).
% 9.53/1.88 thf(f5649,plain,(
% 9.53/1.88 ( ! [X0 : $i] : (($true = ((cN @ (sK2 @ cN @ cN)))) | (((cN @ X0)) = $true) | ($true != ((cODD @ X0)))) ) | (~spl3_2 | ~spl3_8)),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f5648])).
% 9.53/1.88 thf(f5666,plain,(
% 9.53/1.88 ( ! [X0 : $i] : ((((cN @ X0)) = $true) | ($true != ((cODD @ X0)))) ) | (~spl3_2 | ~spl3_8 | ~spl3_34)),
% 9.53/1.88 inference(forward_subsumption_resolution,[],[f5649,f1351])).
% 9.53/1.88 thf(f5669,plain,(
% 9.53/1.88 spl3_9 | ~spl3_2 | ~spl3_8 | ~spl3_34),
% 9.53/1.88 inference(avatar_split_clause,[],[f5666,f1248,f290,f28,f293])).
% 9.53/1.88 thf(f5683,plain,(
% 9.53/1.88 $false | (~spl3_2 | ~spl3_8 | ~spl3_33)),
% 9.53/1.88 inference(forward_subsumption_resolution,[],[f1251,f4124])).
% 9.53/1.88 thf(f5684,plain,(
% 9.53/1.88 ~spl3_2 | ~spl3_8 | ~spl3_33),
% 9.53/1.88 inference(avatar_contradiction_clause,[],[f5683])).
% 9.53/1.88 thf(f5707,plain,(
% 9.53/1.88 ($true != ((cODD @ sK0))) | ~spl3_9),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f296])).
% 9.53/1.88 thf(f5717,plain,(
% 9.53/1.88 ~spl3_2 | ~spl3_9),
% 9.53/1.88 inference(avatar_split_clause,[],[f5707,f293,f28])).
% 9.53/1.88 thf(f5719,definition,(
% 9.53/1.88 spl3_86 <=> ($true = ((cN @ (sK1 @ cN @ cN))))),
% 9.53/1.88 introduced(definition,[new_symbols(definition,[spl3_86])],[avatar_definition])).
% 9.53/1.88 thf(f5720,plain,(
% 9.53/1.88 ($true != ((cN @ (sK1 @ cN @ cN)))) | spl3_86),
% 9.53/1.88 inference(avatar_component_clause,[],[f5719])).
% 9.53/1.88 thf(f6651,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true != ((cEVEN @ X1))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | ($true != (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ c0))) | ($true != ((cN @ X2))) | (((sK2 @ cN @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))) != X2) | (((cN @ X0)) != $true) | (((sK1 @ cN @ cN)) != X0)) )),
% 9.53/1.88 inference(constrained_superposition,[],[f496,f18])).
% 9.53/1.88 thf(f6685,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((cEVEN @ X1))) | ($true = (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | ($true != (((^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ c0))) | ($true != ((cN @ X2))) | (((sK2 @ cN @ (^[Y0 : $i]: (cN @ ((^[Y1 : $i]: (Y1)) @ Y0))))) != X2) | (((cN @ X0)) != $true) | (((sK1 @ cN @ cN)) != X0)) )),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f6651])).
% 9.53/1.88 thf(f6686,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((cEVEN @ X1))) | ($true = ((cN @ X1))) | (((cN @ c0)) != $true) | ($true != ((cN @ X2))) | (((sK2 @ cN @ cN)) != X2) | (((cN @ X0)) != $true) | (((sK1 @ cN @ cN)) != X0)) )),
% 9.53/1.88 inference(beta-eta_normalization,[],[f6685])).
% 9.53/1.88 thf(f6727,plain,(
% 9.53/1.88 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((cEVEN @ X1))) | ($true = ((cN @ X1))) | ($true != ((cN @ X2))) | (((sK2 @ cN @ cN)) != X2) | (((cN @ X0)) != $true) | (((sK1 @ cN @ cN)) != X0)) )),
% 9.53/1.88 inference(forward_subsumption_resolution,[],[f6686,f17])).
% 9.53/1.88 thf(f6739,plain,(
% 9.53/1.88 spl3_33 | spl3_34 | spl3_4),
% 9.53/1.88 inference(avatar_split_clause,[],[f6727,f84,f1248,f1245])).
% 9.53/1.88 thf(f6741,plain,(
% 9.53/1.88 ($true != ((cN @ (sK1 @ cN @ cN)))) | (~spl3_7 | ~spl3_34)),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f3195])).
% 9.53/1.88 thf(f6765,plain,(
% 9.53/1.88 ~spl3_86 | ~spl3_7 | ~spl3_34),
% 9.53/1.88 inference(avatar_split_clause,[],[f6741,f1248,f222,f5719])).
% 9.53/1.88 thf(f6778,plain,(
% 9.53/1.88 ~spl3_86 | ~spl3_33),
% 9.53/1.88 inference(avatar_split_clause,[],[f1251,f1245,f5719])).
% 9.53/1.88 thf(f6809,plain,(
% 9.53/1.88 ( ! [X0 : ($i > $o),X1 : $i] : (($true != ((cN @ (sK2 @ cN @ X0)))) | ($true = ((X0 @ X1))) | (((X0 @ c0)) != $true) | ($true = ((cN @ (sK1 @ cN @ X0)))) | ($true != ((cEVEN @ X1)))) )),
% 9.53/1.88 inference(equality_resolution,[],[f159])).
% 9.53/1.88 thf(f7859,plain,(
% 9.53/1.88 ( ! [X0 : $i] : (($true != $true) | (((cN @ X0)) = $true) | (((cN @ c0)) != $true) | ($true = ((cN @ (sK1 @ cN @ cN)))) | ($true != ((cEVEN @ X0))) | ($true = ((cN @ (sK1 @ cN @ cN))))) ) | ~spl3_3),
% 9.53/1.88 inference(constrained_superposition,[],[f6809,f82])).
% 9.53/1.88 thf(f7865,plain,(
% 9.53/1.88 ( ! [X0 : $i] : (($true != $true) | (((cN @ X0)) = $true) | (((cN @ c0)) != $true) | ($true = ((cN @ (sK1 @ cN @ cN)))) | ($true != ((cEVEN @ X0)))) ) | ~spl3_3),
% 9.53/1.88 inference(duplicate_literal_removal,[],[f7859])).
% 9.53/1.88 thf(f7866,plain,(
% 9.53/1.88 ( ! [X0 : $i] : ((((cN @ X0)) = $true) | (((cN @ c0)) != $true) | ($true = ((cN @ (sK1 @ cN @ cN)))) | ($true != ((cEVEN @ X0)))) ) | ~spl3_3),
% 9.53/1.88 inference(trivial_inequality_removal,[],[f7865])).
% 9.53/1.88 thf(f7881,plain,(
% 9.53/1.88 ( ! [X0 : $i] : ((((cN @ X0)) = $true) | ($true = ((cN @ (sK1 @ cN @ cN)))) | ($true != ((cEVEN @ X0)))) ) | ~spl3_3),
% 9.53/1.88 inference(forward_subsumption_resolution,[],[f7866,f17])).
% 9.53/1.88 thf(f7884,plain,(
% 9.53/1.88 ( ! [X0 : $i] : ((((cN @ X0)) = $true) | ($true != ((cEVEN @ X0)))) ) | (~spl3_3 | spl3_86)),
% 9.53/1.88 inference(forward_subsumption_resolution,[],[f7881,f5720])).
% 9.53/1.88 thf(f7887,plain,(
% 9.53/1.88 spl3_4 | ~spl3_3 | spl3_86),
% 9.53/1.88 inference(avatar_split_clause,[],[f7884,f5719,f81,f84])).
% 9.53/1.88 cnf(s1, plain, spl3_1 | spl3_2, inference(sat_conversion,[],[f31])).
% 9.53/1.88 cnf(s2, plain, spl3_3 | spl3_4, inference(sat_conversion,[],[f86])).
% 9.53/1.88 cnf(s5, plain, spl3_4 | spl3_7, inference(sat_conversion,[],[f224])).
% 9.53/1.88 cnf(s9, plain, spl3_8 | spl3_9, inference(sat_conversion,[],[f295])).
% 9.53/1.88 cnf(s28, plain, spl3_9 | spl3_20, inference(sat_conversion,[],[f644])).
% 9.53/1.88 cnf(s61, plain, ~spl3_20 | spl3_33 | spl3_34, inference(sat_conversion,[],[f1250])).
% 9.53/1.88 cnf(s127, plain, ~spl3_1 | ~spl3_4, inference(sat_conversion,[],[f3283])).
% 9.53/1.88 cnf(s225, plain, ~spl3_2 | ~spl3_8 | spl3_9 | ~spl3_34, inference(sat_conversion,[],[f5669])).
% 9.53/1.88 cnf(s228, plain, ~spl3_2 | ~spl3_8 | ~spl3_33, inference(sat_conversion,[],[f5684])).
% 9.53/1.88 cnf(s241, plain, ~spl3_2 | ~spl3_9, inference(sat_conversion,[],[f5717])).
% 9.53/1.88 cnf(s300, plain, spl3_4 | spl3_33 | spl3_34, inference(sat_conversion,[],[f6739])).
% 9.53/1.88 cnf(s319, plain, ~spl3_7 | ~spl3_34 | ~spl3_86, inference(sat_conversion,[],[f6765])).
% 9.53/1.88 cnf(s323, plain, ~spl3_33 | ~spl3_86, inference(sat_conversion,[],[f6778])).
% 9.53/1.88 cnf(s343, plain, ~spl3_3 | spl3_4 | spl3_86, inference(sat_conversion,[],[f7887])).
% 9.53/1.88 cnf(s352, plain, ~spl3_2, inference(rat,[],[s61,s225,s228,s9,s28,s241])).
% 9.53/1.88 cnf(s353, plain, spl3_1, inference(rat,[],[s1,s352])).
% 9.53/1.88 cnf(s354, plain, ~spl3_4, inference(rat,[],[s127,s353])).
% 9.53/1.88 cnf(s363, plain, spl3_7, inference(rat,[],[s5,s354])).
% 9.53/1.88 cnf(s364, plain, spl3_3, inference(rat,[],[s2,s354])).
% 9.53/1.88 cnf(s370, plain, spl3_86, inference(rat,[],[s343,s354,s364])).
% 9.53/1.88 cnf(s378, plain, ~spl3_33, inference(rat,[],[s323,s370])).
% 9.53/1.88 cnf(s379, plain, ~spl3_34, inference(rat,[],[s319,s363,s370])).
% 9.53/1.88 cnf(s380, plain, $false, inference(rat,[],[s300,s354,s378,s379])).
% 9.53/1.88 thf(f7888,plain,(
% 9.53/1.88 $false),
% 9.53/1.88 inference(avatar_sat_refutation,[],[s380])).
% 9.53/1.88 % SZS output end Proof for theBenchmark
% 9.53/1.88 % (1242002)------------------------------
% 9.53/1.88 % (1242002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.53/1.88 % (1242002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.53/1.88 % (1242002)CaDiCaL version: 2.1.3
% 9.53/1.88 % (1242002)Termination reason: Refutation
% 9.53/1.88 % (1242002)Time elapsed: 0.484 s
% 9.53/1.88 % (1242002)Peak memory usage: 16 MB
% 9.53/1.88 % (1242002)Instructions burned: 1004 (million)
% 9.53/1.88 % (1241933)Success in time 1.645 s
% 9.53/1.88 % Vampire exiting
%------------------------------------------------------------------------------