%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO391^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:49:51 AM UTC 2026
% Result : Theorem 12.83s 2.09s
% Output : Refutation 12.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO391^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.17 % Computer : n014.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Tue Sep 29 16:50:15 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 Running first-order model finding
% 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.49/0.90 % (2919123)Will run a generic schedule for satisfiability detection.
% 3.49/0.90 % (2919151)dis+10_1_sil=32000:sp=arity:random_seed=4242145661:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.49/0.90 % (2919148)% WARNING: option uhcvi not known.
% 3.49/0.90 % (2919147)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3375701577_2999 on theBenchmark for (2999ds/0Mi)
% 3.49/0.90 % (2919148)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1195171684:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.49/0.90 % (2919149)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3497555651:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.49/0.90 % (2919152)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=689978655:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.49/0.90 % (2919154)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1361068966:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.49/0.90 % (2919153)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=317714132:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.84/0.90 % (2919148)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.84/0.90 % Exception at run slice level
% 3.84/0.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.84/0.90 % (2919152)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.84/0.90 % (2919148)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.84/0.90 % (2919151)Instruction limit reached!
% 3.84/0.90 % (2919151)------------------------------
% 3.84/0.90 % (2919151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.90 % (2919151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.90 % (2919151)CaDiCaL version: 2.1.3
% 3.84/0.90 % (2919151)Termination reason: Instruction limit
% 3.84/0.90 % (2919151)Termination phase: Saturation
% 3.84/0.90 % (2919151)Time elapsed: 0.029 s
% 3.84/0.90 % (2919151)Peak memory usage: 12 MB
% 3.84/0.90 % (2919151)Instructions burned: 107 (million)
% 3.84/0.90 % (2919168)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=42479737:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.84/0.90 % Exception at run slice level
% 3.84/0.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.84/0.90 % (2919171)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=22049294:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.84/0.90 % (2919173)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=3950161052:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.84/0.90 % (2919173)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.84/0.90 % (2919173)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.84/0.90 % (2919152)Instruction limit reached!
% 3.84/0.90 % (2919152)------------------------------
% 3.84/0.90 % (2919152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.90 % (2919152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.90 % (2919152)CaDiCaL version: 2.1.3
% 3.84/0.90 % (2919152)Termination reason: Instruction limit
% 3.84/0.90 % (2919152)Termination phase: Saturation
% 3.84/0.90 % (2919152)Time elapsed: 0.054 s
% 3.84/0.90 % (2919152)Peak memory usage: 12 MB
% 3.84/0.90 % (2919152)Instructions burned: 117 (million)
% 3.84/0.90 % (2919153)Instruction limit reached!
% 3.84/0.90 % (2919153)------------------------------
% 3.84/0.90 % (2919153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.90 % (2919153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.90 % (2919153)CaDiCaL version: 2.1.3
% 3.84/0.90 % (2919153)Termination reason: Instruction limit
% 3.84/0.90 % (2919153)Termination phase: Saturation
% 3.84/0.90 % (2919153)Time elapsed: 0.064 s
% 3.84/0.90 % (2919153)Peak memory usage: 12 MB
% 3.84/0.90 % (2919153)Instructions burned: 132 (million)
% 3.84/0.90 % (2919171)Instruction limit reached!
% 3.84/0.90 % (2919171)------------------------------
% 3.84/0.90 % (2919171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.83/2.09 % (2919171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.09 % (2919171)CaDiCaL version: 2.1.3
% 12.83/2.09 % (2919171)Termination reason: Instruction limit
% 12.83/2.09 % (2919171)Termination phase: Saturation
% 12.83/2.09 % (2919171)Time elapsed: 0.037 s
% 12.83/2.09 % (2919171)Peak memory usage: 12 MB
% 12.83/2.09 % (2919171)Instructions burned: 133 (million)
% 12.83/2.09 % (2919176)ott-21_1_sil=16000:fs=off:random_seed=1969141862:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 12.83/2.09 % (2919154)Instruction limit reached!
% 12.83/2.09 % (2919154)------------------------------
% 12.83/2.09 % (2919154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.83/2.09 % (2919154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.09 % (2919154)CaDiCaL version: 2.1.3
% 12.83/2.09 % (2919154)Termination reason: Instruction limit
% 12.83/2.09 % (2919154)Termination phase: Saturation
% 12.83/2.09 % (2919154)Time elapsed: 0.077 s
% 12.83/2.09 % (2919154)Peak memory usage: 12 MB
% 12.83/2.09 % (2919154)Instructions burned: 159 (million)
% 12.83/2.09 % (2919178)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3124727805:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 12.83/2.09 % Exception at run slice level
% 12.83/2.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 12.83/2.09 % (2919177)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1001376495:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 12.83/2.09 % (2919182)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3889587308:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 12.83/2.09 % Exception at run slice level
% 12.83/2.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 12.83/2.09 % (2919180)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=282916630:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 12.83/2.09 % (2919185)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=1516404098:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 12.83/2.09 % (2919185)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 12.83/2.09 % (2919176)Instruction limit reached!
% 12.83/2.09 % (2919176)------------------------------
% 12.83/2.09 % (2919176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.83/2.09 % (2919176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.09 % (2919176)CaDiCaL version: 2.1.3
% 12.83/2.09 % (2919176)Termination reason: Instruction limit
% 12.83/2.09 % (2919176)Termination phase: Saturation
% 12.83/2.09 % (2919176)Time elapsed: 0.076 s
% 12.83/2.09 % (2919176)Peak memory usage: 12 MB
% 12.83/2.09 % (2919176)Instructions burned: 180 (million)
% 12.83/2.09 % (2919188)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2595086944:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 12.83/2.09 % (2919188)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 12.83/2.09 % (2919185)Instruction limit reached!
% 12.83/2.09 % (2919185)------------------------------
% 12.83/2.09 % (2919185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.83/2.09 % (2919185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.09 % (2919185)CaDiCaL version: 2.1.3
% 12.83/2.09 % (2919185)Termination reason: Instruction limit
% 12.83/2.09 % (2919185)Termination phase: Saturation
% 12.83/2.09 % (2919185)Time elapsed: 0.164 s
% 12.83/2.09 % (2919185)Peak memory usage: 14 MB
% 12.83/2.09 % (2919185)Instructions burned: 693 (million)
% 12.83/2.09 % (2919190)fmb+10_1_sil=64000:random_seed=863584929:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 12.83/2.09 % (2919190)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 12.83/2.09 % Exception at run slice level
% 12.83/2.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 12.83/2.09 % (2919192)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1138614310:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 12.83/2.09 % Exception at run slice level
% 12.83/2.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 12.83/2.09 % (2919194)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=574480184:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 12.83/2.09 % Exception at run slice level
% 12.83/2.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 12.83/2.09 % (2919196)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1761281997:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 12.83/2.09 % (2919196)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 12.83/2.09 % (2919177)Instruction limit reached!
% 12.83/2.09 % (2919177)------------------------------
% 12.83/2.09 % (2919177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.83/2.09 % (2919177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.09 % (2919177)CaDiCaL version: 2.1.3
% 12.83/2.09 % (2919177)Termination reason: Instruction limit
% 12.83/2.09 % (2919177)Termination phase: Saturation
% 12.83/2.09 % (2919177)Time elapsed: 0.240 s
% 12.83/2.09 % (2919177)Peak memory usage: 12 MB
% 12.83/2.09 % (2919177)Instructions burned: 477 (million)
% 12.83/2.09 % (2919198)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3733051054:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 12.83/2.09 % (2919198)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 12.83/2.09 % (2919198)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 12.83/2.09 % (2919173)Instruction limit reached!
% 12.83/2.09 % (2919173)------------------------------
% 12.83/2.09 % (2919173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.83/2.09 % (2919173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.09 % (2919173)CaDiCaL version: 2.1.3
% 12.83/2.09 % (2919173)Termination reason: Instruction limit
% 12.83/2.09 % (2919173)Termination phase: Saturation
% 12.83/2.09 % (2919173)Time elapsed: 0.303 s
% 12.83/2.09 % (2919173)Peak memory usage: 13 MB
% 12.83/2.09 % (2919173)Instructions burned: 685 (million)
% 12.83/2.09 % (2919200)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=535831029:i=6324_2996 on theBenchmark for (2996ds/6324Mi)
% 12.83/2.09 % Exception at run slice level
% 12.83/2.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 12.83/2.09 % (2919202)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=411816545:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 12.83/2.09 % Exception at run slice level
% 12.83/2.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 12.83/2.09 % (2919204)ott-2_1_sil=16000:newcnf=on:random_seed=3139978632:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi)
% 12.83/2.09 % (2919204)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 12.83/2.09 % (2919188)Instruction limit reached!
% 12.83/2.09 % (2919188)------------------------------
% 12.83/2.09 % (2919188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.83/2.09 % (2919188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.09 % (2919188)CaDiCaL version: 2.1.3
% 12.83/2.09 % (2919188)Termination reason: Instruction limit
% 12.83/2.09 % (2919188)Termination phase: Saturation
% 12.83/2.09 % (2919188)Time elapsed: 0.417 s
% 12.83/2.09 % (2919188)Peak memory usage: 14 MB
% 12.83/2.09 % (2919188)Instructions burned: 879 (million)
% 12.83/2.09 % (2919206)ott+10_1_sil=32000:tgt=ground:random_seed=3861958077:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 12.83/2.09 % (2919180)Instruction limit reached!
% 12.83/2.09 % (2919180)------------------------------
% 12.83/2.09 % (2919180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.83/2.09 % (2919180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.09 % (2919180)CaDiCaL version: 2.1.3
% 12.83/2.09 % (2919180)Termination reason: Instruction limit
% 12.83/2.09 % (2919180)Termination phase: Saturation
% 12.83/2.09 % (2919180)Time elapsed: 0.530 s
% 12.83/2.09 % (2919180)Peak memory usage: 14 MB
% 12.83/2.09 % (2919180)Instructions burned: 1180 (million)
% 12.83/2.09 % (2919208)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1303587255:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 12.83/2.09 % Exception at run slice level
% 12.83/2.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 12.83/2.09 % (2919210)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4113481638:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 12.83/2.09 % (2919210)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 12.83/2.09 % (2919204)Instruction limit reached!
% 12.83/2.09 % (2919204)------------------------------
% 12.83/2.09 % (2919204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.83/2.09 % (2919204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.09 % (2919204)CaDiCaL version: 2.1.3
% 12.83/2.09 % (2919204)Termination reason: Instruction limit
% 12.83/2.09 % (2919204)Termination phase: Saturation
% 12.83/2.09 % (2919204)Time elapsed: 0.386 s
% 12.83/2.09 % (2919204)Peak memory usage: 13 MB
% 12.83/2.09 % (2919204)Instructions burned: 869 (million)
% 12.83/2.09 % (2919212)dis+21_1_sil=32000:sas=cadical:random_seed=3107813474:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi)
% 12.83/2.09 % (2919198)Instruction limit reached!
% 12.83/2.09 % (2919198)------------------------------
% 12.83/2.09 % (2919198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.83/2.09 % (2919198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.09 % (2919198)CaDiCaL version: 2.1.3
% 12.83/2.09 % (2919198)Termination reason: Instruction limit
% 12.83/2.09 % (2919198)Termination phase: Saturation
% 12.83/2.09 % (2919198)Time elapsed: 0.684 s
% 12.83/2.09 % (2919198)Peak memory usage: 15 MB
% 12.83/2.09 % (2919198)Instructions burned: 1473 (million)
% 12.83/2.09 % (2919214)ott+11_1_sil=16000:gs=on:random_seed=3911855474:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi)
% 12.83/2.09 % (2919214)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 12.83/2.09 % (2919196)Instruction limit reached!
% 12.83/2.09 % (2919196)------------------------------
% 12.83/2.09 % (2919196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.83/2.09 % (2919196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.09 % (2919196)CaDiCaL version: 2.1.3
% 12.83/2.09 % (2919196)Termination reason: Instruction limit
% 12.83/2.09 % (2919196)Termination phase: Saturation
% 12.83/2.09 % (2919196)Time elapsed: 1.183 s
% 12.83/2.09 % (2919196)Peak memory usage: 17 MB
% 12.83/2.09 % (2919196)Instructions burned: 5132 (million)
% 12.83/2.09 % (2919216)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=102531156:fmbsr=1.6:i=67534_2984 on theBenchmark for (2984ds/67534Mi)
% 12.83/2.09 % Exception at run slice level
% 12.83/2.09 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 12.83/2.09 % (2919218)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=127569142:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2984 on theBenchmark for (2984ds/4591Mi)
% 12.83/2.09 % (2919148) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2919123-2919148"...
% 12.83/2.09 % (2919148)...printing done.
% 12.83/2.09 % (2919148)Refutation found. Thanks to Tanya!
% 12.83/2.09 % SZS status Theorem for theBenchmark
% 12.83/2.09 % SZS output start Proof for theBenchmark
% 12.83/2.09 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 12.83/2.09 thf(func_def_0, type, cQ_7: ($i > $i > $i > $o)).
% 12.83/2.09 thf(func_def_1, type, f: ($i > $i)).
% 12.83/2.09 thf(func_def_2, type, cP_6: ($i > $i > $o)).
% 12.83/2.09 thf(func_def_3, type, cQ_6: ($i > $i > $i > $o)).
% 12.83/2.09 thf(func_def_8, type, cP_5: ($i > $i > $o)).
% 12.83/2.09 thf(func_def_9, type, cQ_5: ($i > $i > $i > $o)).
% 12.83/2.09 thf(func_def_10, type, cP_4: ($i > $i > $o)).
% 12.83/2.09 thf(func_def_11, type, cQ_4: ($i > $i > $i > $o)).
% 12.83/2.09 thf(func_def_12, type, cP_3: ($i > $i > $o)).
% 12.83/2.09 thf(func_def_13, type, cQ_3: ($i > $i > $i > $o)).
% 12.83/2.09 thf(func_def_14, type, cP_2: ($i > $i > $o)).
% 12.83/2.09 thf(func_def_15, type, cQ_2: ($i > $i > $i > $o)).
% 12.83/2.09 thf(func_def_16, type, cP_1: ($i > $i > $o)).
% 12.83/2.09 thf(func_def_17, type, cQ_1: ($i > $i > $i > $o)).
% 12.83/2.09 thf(f1,conjecture,(
% 12.83/2.09 ~(! [X0 : $i,X1 : $i,X2 : $i] : ~(cQ_7 @ X0 @ X1 @ X2) & ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i] : ((cQ_7 @ X3 @ X4 @ X5) | ~(cP_6 @ (f @ X2) @ X5) | ~(cP_6 @ (f @ X1) @ X4) | ~(cP_6 @ (f @ X0) @ X3) | ~(cQ_6 @ X0 @ X1 @ X2)) & ! [X0 : $i,X1 : $i] : ((cP_6 @ (f @ X0) @ X1) | ~(cP_6 @ X0 @ X1)) & ! [X0 : $i] : (cP_6 @ d @ X0) & (cP_6 @ c @ c) & (cP_6 @ b @ b) & (cP_6 @ a @ a) & ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i] : ((cQ_6 @ X3 @ X4 @ X5) | ~(cP_5 @ (f @ X2) @ X5) | ~(cP_5 @ (f @ X1) @ X4) | ~(cP_5 @ (f @ X0) @ X3) | ~(cQ_5 @ X0 @ X1 @ X2)) & ! [X0 : $i,X1 : $i] : ((cP_5 @ (f @ X0) @ X1) | ~(cP_5 @ X0 @ X1)) & ! [X0 : $i] : (cP_5 @ d @ X0) & (cP_5 @ c @ c) & (cP_5 @ b @ b) & (cP_5 @ a @ a) & ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i] : ((cQ_5 @ X3 @ X4 @ X5) | ~(cP_4 @ (f @ X2) @ X5) | ~(cP_4 @ (f @ X1) @ X4) | ~(cP_4 @ (f @ X0) @ X3) | ~(cQ_4 @ X0 @ X1 @ X2)) & ! [X0 : $i,X1 : $i] : ((cP_4 @ (f @ X0) @ X1) | ~(cP_4 @ X0 @ X1)) & ! [X0 : $i] : (cP_4 @ d @ X0) & (cP_4 @ c @ c) & (cP_4 @ b @ b) & (cP_4 @ a @ a) & ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i] : ((cQ_4 @ X3 @ X4 @ X5) | ~(cP_3 @ (f @ X2) @ X5) | ~(cP_3 @ (f @ X1) @ X4) | ~(cP_3 @ (f @ X0) @ X3) | ~(cQ_3 @ X0 @ X1 @ X2)) & ! [X0 : $i,X1 : $i] : ((cP_3 @ (f @ X0) @ X1) | ~(cP_3 @ X0 @ X1)) & ! [X0 : $i] : (cP_3 @ d @ X0) & (cP_3 @ c @ c) & (cP_3 @ b @ b) & (cP_3 @ a @ a) & ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i] : ((cQ_3 @ X3 @ X4 @ X5) | ~(cP_2 @ (f @ X2) @ X5) | ~(cP_2 @ (f @ X1) @ X4) | ~(cP_2 @ (f @ X0) @ X3) | ~(cQ_2 @ X0 @ X1 @ X2)) & ! [X0 : $i,X1 : $i] : ((cP_2 @ (f @ X0) @ X1) | ~(cP_2 @ X0 @ X1)) & ! [X0 : $i] : (cP_2 @ d @ X0) & (cP_2 @ c @ c) & (cP_2 @ b @ b) & (cP_2 @ a @ a) & ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i] : ((cQ_2 @ X3 @ X4 @ X5) | ~(cP_1 @ (f @ X2) @ X5) | ~(cP_1 @ (f @ X1) @ X4) | ~(cP_1 @ (f @ X0) @ X3) | ~(cQ_1 @ X0 @ X1 @ X2)) & ! [X0 : $i,X1 : $i] : ((cP_1 @ (f @ X0) @ X1) | ~(cP_1 @ X0 @ X1)) & ! [X0 : $i] : (cP_1 @ d @ X0) & (cP_1 @ c @ c) & (cP_1 @ b @ b) & (cP_1 @ a @ a) & (cQ_1 @ a @ b @ c))),
% 12.83/2.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM409_6)).
% 12.83/2.09 thf(f2,negated_conjecture,(
% 12.83/2.09 ~ ~(! [X0 : $i,X1 : $i,X2 : $i] : ~(cQ_7 @ X0 @ X1 @ X2) & ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i] : ((cQ_7 @ X3 @ X4 @ X5) | ~(cP_6 @ (f @ X2) @ X5) | ~(cP_6 @ (f @ X1) @ X4) | ~(cP_6 @ (f @ X0) @ X3) | ~(cQ_6 @ X0 @ X1 @ X2)) & ! [X0 : $i,X1 : $i] : ((cP_6 @ (f @ X0) @ X1) | ~(cP_6 @ X0 @ X1)) & ! [X0 : $i] : (cP_6 @ d @ X0) & (cP_6 @ c @ c) & (cP_6 @ b @ b) & (cP_6 @ a @ a) & ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i] : ((cQ_6 @ X3 @ X4 @ X5) | ~(cP_5 @ (f @ X2) @ X5) | ~(cP_5 @ (f @ X1) @ X4) | ~(cP_5 @ (f @ X0) @ X3) | ~(cQ_5 @ X0 @ X1 @ X2)) & ! [X0 : $i,X1 : $i] : ((cP_5 @ (f @ X0) @ X1) | ~(cP_5 @ X0 @ X1)) & ! [X0 : $i] : (cP_5 @ d @ X0) & (cP_5 @ c @ c) & (cP_5 @ b @ b) & (cP_5 @ a @ a) & ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i] : ((cQ_5 @ X3 @ X4 @ X5) | ~(cP_4 @ (f @ X2) @ X5) | ~(cP_4 @ (f @ X1) @ X4) | ~(cP_4 @ (f @ X0) @ X3) | ~(cQ_4 @ X0 @ X1 @ X2)) & ! [X0 : $i,X1 : $i] : ((cP_4 @ (f @ X0) @ X1) | ~(cP_4 @ X0 @ X1)) & ! [X0 : $i] : (cP_4 @ d @ X0) & (cP_4 @ c @ c) & (cP_4 @ b @ b) & (cP_4 @ a @ a) & ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i] : ((cQ_4 @ X3 @ X4 @ X5) | ~(cP_3 @ (f @ X2) @ X5) | ~(cP_3 @ (f @ X1) @ X4) | ~(cP_3 @ (f @ X0) @ X3) | ~(cQ_3 @ X0 @ X1 @ X2)) & ! [X0 : $i,X1 : $i] : ((cP_3 @ (f @ X0) @ X1) | ~(cP_3 @ X0 @ X1)) & ! [X0 : $i] : (cP_3 @ d @ X0) & (cP_3 @ c @ c) & (cP_3 @ b @ b) & (cP_3 @ a @ a) & ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i] : ((cQ_3 @ X3 @ X4 @ X5) | ~(cP_2 @ (f @ X2) @ X5) | ~(cP_2 @ (f @ X1) @ X4) | ~(cP_2 @ (f @ X0) @ X3) | ~(cQ_2 @ X0 @ X1 @ X2)) & ! [X0 : $i,X1 : $i] : ((cP_2 @ (f @ X0) @ X1) | ~(cP_2 @ X0 @ X1)) & ! [X0 : $i] : (cP_2 @ d @ X0) & (cP_2 @ c @ c) & (cP_2 @ b @ b) & (cP_2 @ a @ a) & ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i,X4 : $i,X5 : $i] : ((cQ_2 @ X3 @ X4 @ X5) | ~(cP_1 @ (f @ X2) @ X5) | ~(cP_1 @ (f @ X1) @ X4) | ~(cP_1 @ (f @ X0) @ X3) | ~(cQ_1 @ X0 @ X1 @ X2)) & ! [X0 : $i,X1 : $i] : ((cP_1 @ (f @ X0) @ X1) | ~(cP_1 @ X0 @ X1)) & ! [X0 : $i] : (cP_1 @ d @ X0) & (cP_1 @ c @ c) & (cP_1 @ b @ b) & (cP_1 @ a @ a) & (cQ_1 @ a @ b @ c))),
% 12.83/2.09 inference(negated_conjecture,[status(cth)],[f1])).
% 12.83/2.09 thf(f3,plain,(
% 12.83/2.09 ~ ~(! [X0 : $i,X1 : $i,X2 : $i] : ~(cQ_7 @ X0 @ X1 @ X2) & ! [X3 : $i,X4 : $i,X5 : $i,X6 : $i,X7 : $i,X8 : $i] : ((cQ_7 @ X6 @ X7 @ X8) | ~(cP_6 @ (f @ X5) @ X8) | ~(cP_6 @ (f @ X4) @ X7) | ~(cP_6 @ (f @ X3) @ X6) | ~(cQ_6 @ X3 @ X4 @ X5)) & ! [X9 : $i,X10 : $i] : ((cP_6 @ (f @ X9) @ X10) | ~(cP_6 @ X9 @ X10)) & ! [X11 : $i] : (cP_6 @ d @ X11) & (cP_6 @ c @ c) & (cP_6 @ b @ b) & (cP_6 @ a @ a) & ! [X12 : $i,X13 : $i,X14 : $i,X15 : $i,X16 : $i,X17 : $i] : ((cQ_6 @ X15 @ X16 @ X17) | ~(cP_5 @ (f @ X14) @ X17) | ~(cP_5 @ (f @ X13) @ X16) | ~(cP_5 @ (f @ X12) @ X15) | ~(cQ_5 @ X12 @ X13 @ X14)) & ! [X18 : $i,X19 : $i] : ((cP_5 @ (f @ X18) @ X19) | ~(cP_5 @ X18 @ X19)) & ! [X20 : $i] : (cP_5 @ d @ X20) & (cP_5 @ c @ c) & (cP_5 @ b @ b) & (cP_5 @ a @ a) & ! [X21 : $i,X22 : $i,X23 : $i,X24 : $i,X25 : $i,X26 : $i] : ((cQ_5 @ X24 @ X25 @ X26) | ~(cP_4 @ (f @ X23) @ X26) | ~(cP_4 @ (f @ X22) @ X25) | ~(cP_4 @ (f @ X21) @ X24) | ~(cQ_4 @ X21 @ X22 @ X23)) & ! [X27 : $i,X28 : $i] : ((cP_4 @ (f @ X27) @ X28) | ~(cP_4 @ X27 @ X28)) & ! [X29 : $i] : (cP_4 @ d @ X29) & (cP_4 @ c @ c) & (cP_4 @ b @ b) & (cP_4 @ a @ a) & ! [X30 : $i,X31 : $i,X32 : $i,X33 : $i,X34 : $i,X35 : $i] : ((cQ_4 @ X33 @ X34 @ X35) | ~(cP_3 @ (f @ X32) @ X35) | ~(cP_3 @ (f @ X31) @ X34) | ~(cP_3 @ (f @ X30) @ X33) | ~(cQ_3 @ X30 @ X31 @ X32)) & ! [X36 : $i,X37 : $i] : ((cP_3 @ (f @ X36) @ X37) | ~(cP_3 @ X36 @ X37)) & ! [X38 : $i] : (cP_3 @ d @ X38) & (cP_3 @ c @ c) & (cP_3 @ b @ b) & (cP_3 @ a @ a) & ! [X39 : $i,X40 : $i,X41 : $i,X42 : $i,X43 : $i,X44 : $i] : ((cQ_3 @ X42 @ X43 @ X44) | ~(cP_2 @ (f @ X41) @ X44) | ~(cP_2 @ (f @ X40) @ X43) | ~(cP_2 @ (f @ X39) @ X42) | ~(cQ_2 @ X39 @ X40 @ X41)) & ! [X45 : $i,X46 : $i] : ((cP_2 @ (f @ X45) @ X46) | ~(cP_2 @ X45 @ X46)) & ! [X47 : $i] : (cP_2 @ d @ X47) & (cP_2 @ c @ c) & (cP_2 @ b @ b) & (cP_2 @ a @ a) & ! [X48 : $i,X49 : $i,X50 : $i,X51 : $i,X52 : $i,X53 : $i] : ((cQ_2 @ X51 @ X52 @ X53) | ~(cP_1 @ (f @ X50) @ X53) | ~(cP_1 @ (f @ X49) @ X52) | ~(cP_1 @ (f @ X48) @ X51) | ~(cQ_1 @ X48 @ X49 @ X50)) & ! [X54 : $i,X55 : $i] : ((cP_1 @ (f @ X54) @ X55) | ~(cP_1 @ X54 @ X55)) & ! [X56 : $i] : (cP_1 @ d @ X56) & (cP_1 @ c @ c) & (cP_1 @ b @ b) & (cP_1 @ a @ a) & (cQ_1 @ a @ b @ c))),
% 12.83/2.09 inference(rectify,[],[f2])).
% 12.83/2.09 thf(f4,plain,(
% 12.83/2.09 ~ ~(! [X0 : $i,X1 : $i,X2 : $i] : ~ (((cQ_7 @ X0 @ X1 @ X2)) = $true) & ! [X3 : $i,X4 : $i,X5 : $i,X6 : $i,X7 : $i,X8 : $i] : ((((cQ_7 @ X6 @ X7 @ X8)) = $true) | ~ (((cP_6 @ (f @ X5) @ X8)) = $true) | ~ (((cP_6 @ (f @ X4) @ X7)) = $true) | ~ (((cP_6 @ (f @ X3) @ X6)) = $true) | ~ (((cQ_6 @ X3 @ X4 @ X5)) = $true)) & ! [X9 : $i,X10 : $i] : ((((cP_6 @ (f @ X9) @ X10)) = $true) | ~ (((cP_6 @ X9 @ X10)) = $true)) & ! [X11 : $i] : (((cP_6 @ d @ X11)) = $true) & (((cP_6 @ c @ c)) = $true) & (((cP_6 @ b @ b)) = $true) & (((cP_6 @ a @ a)) = $true) & ! [X12 : $i,X13 : $i,X14 : $i,X15 : $i,X16 : $i,X17 : $i] : ((((cQ_6 @ X15 @ X16 @ X17)) = $true) | ~ (((cP_5 @ (f @ X14) @ X17)) = $true) | ~ (((cP_5 @ (f @ X13) @ X16)) = $true) | ~ (((cP_5 @ (f @ X12) @ X15)) = $true) | ~ (((cQ_5 @ X12 @ X13 @ X14)) = $true)) & ! [X18 : $i,X19 : $i] : ((((cP_5 @ (f @ X18) @ X19)) = $true) | ~ (((cP_5 @ X18 @ X19)) = $true)) & ! [X20 : $i] : (((cP_5 @ d @ X20)) = $true) & (((cP_5 @ c @ c)) = $true) & (((cP_5 @ b @ b)) = $true) & (((cP_5 @ a @ a)) = $true) & ! [X21 : $i,X22 : $i,X23 : $i,X24 : $i,X25 : $i,X26 : $i] : ((((cQ_5 @ X24 @ X25 @ X26)) = $true) | ~ (((cP_4 @ (f @ X23) @ X26)) = $true) | ~ (((cP_4 @ (f @ X22) @ X25)) = $true) | ~ (((cP_4 @ (f @ X21) @ X24)) = $true) | ~ (((cQ_4 @ X21 @ X22 @ X23)) = $true)) & ! [X27 : $i,X28 : $i] : ((((cP_4 @ (f @ X27) @ X28)) = $true) | ~ (((cP_4 @ X27 @ X28)) = $true)) & ! [X29 : $i] : (((cP_4 @ d @ X29)) = $true) & (((cP_4 @ c @ c)) = $true) & (((cP_4 @ b @ b)) = $true) & (((cP_4 @ a @ a)) = $true) & ! [X30 : $i,X31 : $i,X32 : $i,X33 : $i,X34 : $i,X35 : $i] : ((((cQ_4 @ X33 @ X34 @ X35)) = $true) | ~ (((cP_3 @ (f @ X32) @ X35)) = $true) | ~ (((cP_3 @ (f @ X31) @ X34)) = $true) | ~ (((cP_3 @ (f @ X30) @ X33)) = $true) | ~ (((cQ_3 @ X30 @ X31 @ X32)) = $true)) & ! [X36 : $i,X37 : $i] : ((((cP_3 @ (f @ X36) @ X37)) = $true) | ~ (((cP_3 @ X36 @ X37)) = $true)) & ! [X38 : $i] : (((cP_3 @ d @ X38)) = $true) & (((cP_3 @ c @ c)) = $true) & (((cP_3 @ b @ b)) = $true) & (((cP_3 @ a @ a)) = $true) & ! [X39 : $i,X40 : $i,X41 : $i,X42 : $i,X43 : $i,X44 : $i] : ((((cQ_3 @ X42 @ X43 @ X44)) = $true) | ~ (((cP_2 @ (f @ X41) @ X44)) = $true) | ~ (((cP_2 @ (f @ X40) @ X43)) = $true) | ~ (((cP_2 @ (f @ X39) @ X42)) = $true) | ~ (((cQ_2 @ X39 @ X40 @ X41)) = $true)) & ! [X45 : $i,X46 : $i] : ((((cP_2 @ (f @ X45) @ X46)) = $true) | ~ (((cP_2 @ X45 @ X46)) = $true)) & ! [X47 : $i] : (((cP_2 @ d @ X47)) = $true) & (((cP_2 @ c @ c)) = $true) & (((cP_2 @ b @ b)) = $true) & (((cP_2 @ a @ a)) = $true) & ! [X48 : $i,X49 : $i,X50 : $i,X51 : $i,X52 : $i,X53 : $i] : ((((cQ_2 @ X51 @ X52 @ X53)) = $true) | ~ (((cP_1 @ (f @ X50) @ X53)) = $true) | ~ (((cP_1 @ (f @ X49) @ X52)) = $true) | ~ (((cP_1 @ (f @ X48) @ X51)) = $true) | ~ (((cQ_1 @ X48 @ X49 @ X50)) = $true)) & ! [X54 : $i,X55 : $i] : ((((cP_1 @ (f @ X54) @ X55)) = $true) | ~ (((cP_1 @ X54 @ X55)) = $true)) & ! [X56 : $i] : (((cP_1 @ d @ X56)) = $true) & (((cP_1 @ c @ c)) = $true) & (((cP_1 @ b @ b)) = $true) & (((cP_1 @ a @ a)) = $true) & (((cQ_1 @ a @ b @ c)) = $true))),
% 12.83/2.09 inference(fool_elimination,[],[f3])).
% 12.83/2.09 thf(f5,plain,(
% 12.83/2.09 ! [X0 : $i,X1 : $i,X2 : $i] : (((cQ_7 @ X0 @ X1 @ X2)) != $true) & ! [X3 : $i,X4 : $i,X5 : $i,X6 : $i,X7 : $i,X8 : $i] : ((((cQ_7 @ X6 @ X7 @ X8)) = $true) | (((cP_6 @ (f @ X5) @ X8)) != $true) | (((cP_6 @ (f @ X4) @ X7)) != $true) | (((cP_6 @ (f @ X3) @ X6)) != $true) | (((cQ_6 @ X3 @ X4 @ X5)) != $true)) & ! [X9 : $i,X10 : $i] : ((((cP_6 @ (f @ X9) @ X10)) = $true) | (((cP_6 @ X9 @ X10)) != $true)) & ! [X11 : $i] : (((cP_6 @ d @ X11)) = $true) & (((cP_6 @ c @ c)) = $true) & (((cP_6 @ b @ b)) = $true) & (((cP_6 @ a @ a)) = $true) & ! [X12 : $i,X13 : $i,X14 : $i,X15 : $i,X16 : $i,X17 : $i] : ((((cQ_6 @ X15 @ X16 @ X17)) = $true) | (((cP_5 @ (f @ X14) @ X17)) != $true) | (((cP_5 @ (f @ X13) @ X16)) != $true) | (((cP_5 @ (f @ X12) @ X15)) != $true) | (((cQ_5 @ X12 @ X13 @ X14)) != $true)) & ! [X18 : $i,X19 : $i] : ((((cP_5 @ (f @ X18) @ X19)) = $true) | (((cP_5 @ X18 @ X19)) != $true)) & ! [X20 : $i] : (((cP_5 @ d @ X20)) = $true) & (((cP_5 @ c @ c)) = $true) & (((cP_5 @ b @ b)) = $true) & (((cP_5 @ a @ a)) = $true) & ! [X21 : $i,X22 : $i,X23 : $i,X24 : $i,X25 : $i,X26 : $i] : ((((cQ_5 @ X24 @ X25 @ X26)) = $true) | (((cP_4 @ (f @ X23) @ X26)) != $true) | (((cP_4 @ (f @ X22) @ X25)) != $true) | (((cP_4 @ (f @ X21) @ X24)) != $true) | (((cQ_4 @ X21 @ X22 @ X23)) != $true)) & ! [X27 : $i,X28 : $i] : ((((cP_4 @ (f @ X27) @ X28)) = $true) | (((cP_4 @ X27 @ X28)) != $true)) & ! [X29 : $i] : (((cP_4 @ d @ X29)) = $true) & (((cP_4 @ c @ c)) = $true) & (((cP_4 @ b @ b)) = $true) & (((cP_4 @ a @ a)) = $true) & ! [X30 : $i,X31 : $i,X32 : $i,X33 : $i,X34 : $i,X35 : $i] : ((((cQ_4 @ X33 @ X34 @ X35)) = $true) | (((cP_3 @ (f @ X32) @ X35)) != $true) | (((cP_3 @ (f @ X31) @ X34)) != $true) | (((cP_3 @ (f @ X30) @ X33)) != $true) | (((cQ_3 @ X30 @ X31 @ X32)) != $true)) & ! [X36 : $i,X37 : $i] : ((((cP_3 @ (f @ X36) @ X37)) = $true) | (((cP_3 @ X36 @ X37)) != $true)) & ! [X38 : $i] : (((cP_3 @ d @ X38)) = $true) & (((cP_3 @ c @ c)) = $true) & (((cP_3 @ b @ b)) = $true) & (((cP_3 @ a @ a)) = $true) & ! [X39 : $i,X40 : $i,X41 : $i,X42 : $i,X43 : $i,X44 : $i] : ((((cQ_3 @ X42 @ X43 @ X44)) = $true) | (((cP_2 @ (f @ X41) @ X44)) != $true) | (((cP_2 @ (f @ X40) @ X43)) != $true) | (((cP_2 @ (f @ X39) @ X42)) != $true) | (((cQ_2 @ X39 @ X40 @ X41)) != $true)) & ! [X45 : $i,X46 : $i] : ((((cP_2 @ (f @ X45) @ X46)) = $true) | (((cP_2 @ X45 @ X46)) != $true)) & ! [X47 : $i] : (((cP_2 @ d @ X47)) = $true) & (((cP_2 @ c @ c)) = $true) & (((cP_2 @ b @ b)) = $true) & (((cP_2 @ a @ a)) = $true) & ! [X48 : $i,X49 : $i,X50 : $i,X51 : $i,X52 : $i,X53 : $i] : ((((cQ_2 @ X51 @ X52 @ X53)) = $true) | (((cP_1 @ (f @ X50) @ X53)) != $true) | (((cP_1 @ (f @ X49) @ X52)) != $true) | (((cP_1 @ (f @ X48) @ X51)) != $true) | (((cQ_1 @ X48 @ X49 @ X50)) != $true)) & ! [X54 : $i,X55 : $i] : ((((cP_1 @ (f @ X54) @ X55)) = $true) | (((cP_1 @ X54 @ X55)) != $true)) & ! [X56 : $i] : (((cP_1 @ d @ X56)) = $true) & (((cP_1 @ c @ c)) = $true) & (((cP_1 @ b @ b)) = $true) & (((cP_1 @ a @ a)) = $true) & (((cQ_1 @ a @ b @ c)) = $true)),
% 12.83/2.09 inference(flattening,[],[f4])).
% 12.83/2.09 thf(f6,plain,(
% 12.83/2.09 (((cQ_1 @ a @ b @ c)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f7,plain,(
% 12.83/2.09 (((cP_1 @ a @ a)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f8,plain,(
% 12.83/2.09 (((cP_1 @ b @ b)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f9,plain,(
% 12.83/2.09 (((cP_1 @ c @ c)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f11,plain,(
% 12.83/2.09 ( ! [X54 : $i,X55 : $i] : ((((cP_1 @ X54 @ X55)) != $true) | (((cP_1 @ (f @ X54) @ X55)) = $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f12,plain,(
% 12.83/2.09 ( ! [X50 : $i,X51 : $i,X48 : $i,X49 : $i,X52 : $i,X53 : $i] : ((((cQ_1 @ X48 @ X49 @ X50)) != $true) | (((cP_1 @ (f @ X50) @ X53)) != $true) | (((cP_1 @ (f @ X49) @ X52)) != $true) | (((cP_1 @ (f @ X48) @ X51)) != $true) | (((cQ_2 @ X51 @ X52 @ X53)) = $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f13,plain,(
% 12.83/2.09 (((cP_2 @ a @ a)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f14,plain,(
% 12.83/2.09 (((cP_2 @ b @ b)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f15,plain,(
% 12.83/2.09 (((cP_2 @ c @ c)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f17,plain,(
% 12.83/2.09 ( ! [X46 : $i,X45 : $i] : ((((cP_2 @ X45 @ X46)) != $true) | (((cP_2 @ (f @ X45) @ X46)) = $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f18,plain,(
% 12.83/2.09 ( ! [X40 : $i,X41 : $i,X39 : $i,X44 : $i,X42 : $i,X43 : $i] : ((((cQ_2 @ X39 @ X40 @ X41)) != $true) | (((cP_2 @ (f @ X41) @ X44)) != $true) | (((cP_2 @ (f @ X40) @ X43)) != $true) | (((cP_2 @ (f @ X39) @ X42)) != $true) | (((cQ_3 @ X42 @ X43 @ X44)) = $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f19,plain,(
% 12.83/2.09 (((cP_3 @ a @ a)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f20,plain,(
% 12.83/2.09 (((cP_3 @ b @ b)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f21,plain,(
% 12.83/2.09 (((cP_3 @ c @ c)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f23,plain,(
% 12.83/2.09 ( ! [X36 : $i,X37 : $i] : ((((cP_3 @ X36 @ X37)) != $true) | (((cP_3 @ (f @ X36) @ X37)) = $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f24,plain,(
% 12.83/2.09 ( ! [X31 : $i,X34 : $i,X35 : $i,X32 : $i,X30 : $i,X33 : $i] : ((((cQ_3 @ X30 @ X31 @ X32)) != $true) | (((cP_3 @ (f @ X32) @ X35)) != $true) | (((cP_3 @ (f @ X31) @ X34)) != $true) | (((cP_3 @ (f @ X30) @ X33)) != $true) | (((cQ_4 @ X33 @ X34 @ X35)) = $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f25,plain,(
% 12.83/2.09 (((cP_4 @ a @ a)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f26,plain,(
% 12.83/2.09 (((cP_4 @ b @ b)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f27,plain,(
% 12.83/2.09 (((cP_4 @ c @ c)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f29,plain,(
% 12.83/2.09 ( ! [X28 : $i,X27 : $i] : ((((cP_4 @ X27 @ X28)) != $true) | (((cP_4 @ (f @ X27) @ X28)) = $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f30,plain,(
% 12.83/2.09 ( ! [X21 : $i,X26 : $i,X24 : $i,X22 : $i,X25 : $i,X23 : $i] : ((((cQ_4 @ X21 @ X22 @ X23)) != $true) | (((cP_4 @ (f @ X23) @ X26)) != $true) | (((cP_4 @ (f @ X22) @ X25)) != $true) | (((cP_4 @ (f @ X21) @ X24)) != $true) | (((cQ_5 @ X24 @ X25 @ X26)) = $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f31,plain,(
% 12.83/2.09 (((cP_5 @ a @ a)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f32,plain,(
% 12.83/2.09 (((cP_5 @ b @ b)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f33,plain,(
% 12.83/2.09 (((cP_5 @ c @ c)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f35,plain,(
% 12.83/2.09 ( ! [X18 : $i,X19 : $i] : ((((cP_5 @ X18 @ X19)) != $true) | (((cP_5 @ (f @ X18) @ X19)) = $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f36,plain,(
% 12.83/2.09 ( ! [X16 : $i,X14 : $i,X17 : $i,X15 : $i,X12 : $i,X13 : $i] : ((((cQ_5 @ X12 @ X13 @ X14)) != $true) | (((cP_5 @ (f @ X14) @ X17)) != $true) | (((cP_5 @ (f @ X13) @ X16)) != $true) | (((cP_5 @ (f @ X12) @ X15)) != $true) | (((cQ_6 @ X15 @ X16 @ X17)) = $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f37,plain,(
% 12.83/2.09 (((cP_6 @ a @ a)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f38,plain,(
% 12.83/2.09 (((cP_6 @ b @ b)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f39,plain,(
% 12.83/2.09 (((cP_6 @ c @ c)) = $true)),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f41,plain,(
% 12.83/2.09 ( ! [X10 : $i,X9 : $i] : ((((cP_6 @ X9 @ X10)) != $true) | (((cP_6 @ (f @ X9) @ X10)) = $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f42,plain,(
% 12.83/2.09 ( ! [X3 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : ((((cQ_7 @ X6 @ X7 @ X8)) = $true) | (((cP_6 @ (f @ X5) @ X8)) != $true) | (((cP_6 @ (f @ X4) @ X7)) != $true) | (((cP_6 @ (f @ X3) @ X6)) != $true) | (((cQ_6 @ X3 @ X4 @ X5)) != $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f43,plain,(
% 12.83/2.09 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((cQ_7 @ X0 @ X1 @ X2)) != $true)) )),
% 12.83/2.09 inference(cnf_transformation,[],[f5])).
% 12.83/2.09 thf(f45,definition,(
% 12.83/2.09 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 12.83/2.09 introduced(theory,[fool_exhaustiveness_axiom])).
% 12.83/2.09 thf(f47,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_1 @ (f @ c) @ c)))),
% 12.83/2.09 inference(constrained_superposition,[],[f11,f9])).
% 12.83/2.09 thf(f48,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_1 @ (f @ b) @ b)))),
% 12.83/2.09 inference(constrained_superposition,[],[f11,f8])).
% 12.83/2.09 thf(f49,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_1 @ (f @ a) @ a)))),
% 12.83/2.09 inference(constrained_superposition,[],[f11,f7])).
% 12.83/2.09 thf(f50,plain,(
% 12.83/2.09 ($true = ((cP_1 @ (f @ a) @ a)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f49])).
% 12.83/2.09 thf(f51,plain,(
% 12.83/2.09 ($true = ((cP_1 @ (f @ b) @ b)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f48])).
% 12.83/2.09 thf(f52,plain,(
% 12.83/2.09 ($true = ((cP_1 @ (f @ c) @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f47])).
% 12.83/2.09 thf(f55,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_2 @ (f @ c) @ c)))),
% 12.83/2.09 inference(constrained_superposition,[],[f17,f15])).
% 12.83/2.09 thf(f56,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_2 @ (f @ b) @ b)))),
% 12.83/2.09 inference(constrained_superposition,[],[f17,f14])).
% 12.83/2.09 thf(f57,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_2 @ (f @ a) @ a)))),
% 12.83/2.09 inference(constrained_superposition,[],[f17,f13])).
% 12.83/2.09 thf(f58,plain,(
% 12.83/2.09 ($true = ((cP_2 @ (f @ a) @ a)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f57])).
% 12.83/2.09 thf(f59,plain,(
% 12.83/2.09 ($true = ((cP_2 @ (f @ b) @ b)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f56])).
% 12.83/2.09 thf(f60,plain,(
% 12.83/2.09 ($true = ((cP_2 @ (f @ c) @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f55])).
% 12.83/2.09 thf(f63,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_3 @ (f @ c) @ c)))),
% 12.83/2.09 inference(constrained_superposition,[],[f23,f21])).
% 12.83/2.09 thf(f64,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_3 @ (f @ b) @ b)))),
% 12.83/2.09 inference(constrained_superposition,[],[f23,f20])).
% 12.83/2.09 thf(f65,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_3 @ (f @ a) @ a)))),
% 12.83/2.09 inference(constrained_superposition,[],[f23,f19])).
% 12.83/2.09 thf(f66,plain,(
% 12.83/2.09 ($true = ((cP_3 @ (f @ a) @ a)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f65])).
% 12.83/2.09 thf(f67,plain,(
% 12.83/2.09 ($true = ((cP_3 @ (f @ b) @ b)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f64])).
% 12.83/2.09 thf(f68,plain,(
% 12.83/2.09 ($true = ((cP_3 @ (f @ c) @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f63])).
% 12.83/2.09 thf(f71,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_4 @ (f @ c) @ c)))),
% 12.83/2.09 inference(constrained_superposition,[],[f29,f27])).
% 12.83/2.09 thf(f72,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_4 @ (f @ b) @ b)))),
% 12.83/2.09 inference(constrained_superposition,[],[f29,f26])).
% 12.83/2.09 thf(f73,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_4 @ (f @ a) @ a)))),
% 12.83/2.09 inference(constrained_superposition,[],[f29,f25])).
% 12.83/2.09 thf(f74,plain,(
% 12.83/2.09 ($true = ((cP_4 @ (f @ a) @ a)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f73])).
% 12.83/2.09 thf(f75,plain,(
% 12.83/2.09 ($true = ((cP_4 @ (f @ b) @ b)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f72])).
% 12.83/2.09 thf(f76,plain,(
% 12.83/2.09 ($true = ((cP_4 @ (f @ c) @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f71])).
% 12.83/2.09 thf(f79,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_5 @ (f @ c) @ c)))),
% 12.83/2.09 inference(constrained_superposition,[],[f35,f33])).
% 12.83/2.09 thf(f80,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_5 @ (f @ b) @ b)))),
% 12.83/2.09 inference(constrained_superposition,[],[f35,f32])).
% 12.83/2.09 thf(f81,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_5 @ (f @ a) @ a)))),
% 12.83/2.09 inference(constrained_superposition,[],[f35,f31])).
% 12.83/2.09 thf(f82,plain,(
% 12.83/2.09 ($true = ((cP_5 @ (f @ a) @ a)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f81])).
% 12.83/2.09 thf(f83,plain,(
% 12.83/2.09 ($true = ((cP_5 @ (f @ b) @ b)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f80])).
% 12.83/2.09 thf(f84,plain,(
% 12.83/2.09 ($true = ((cP_5 @ (f @ c) @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f79])).
% 12.83/2.09 thf(f93,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_6 @ (f @ c) @ c)))),
% 12.83/2.09 inference(constrained_superposition,[],[f41,f39])).
% 12.83/2.09 thf(f94,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_6 @ (f @ b) @ b)))),
% 12.83/2.09 inference(constrained_superposition,[],[f41,f38])).
% 12.83/2.09 thf(f95,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cP_6 @ (f @ a) @ a)))),
% 12.83/2.09 inference(constrained_superposition,[],[f41,f37])).
% 12.83/2.09 thf(f96,plain,(
% 12.83/2.09 ($true = ((cP_6 @ (f @ a) @ a)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f95])).
% 12.83/2.09 thf(f97,plain,(
% 12.83/2.09 ($true = ((cP_6 @ (f @ b) @ b)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f94])).
% 12.83/2.09 thf(f98,plain,(
% 12.83/2.09 ($true = ((cP_6 @ (f @ c) @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f93])).
% 12.83/2.09 thf(f121,plain,(
% 12.83/2.09 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true != ((cP_1 @ (f @ c) @ X0))) | ($true != ((cP_1 @ (f @ b) @ X1))) | ($true != ((cP_1 @ (f @ a) @ X2))) | ($true = ((cQ_2 @ X2 @ X1 @ X0)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f12,f6])).
% 12.83/2.09 thf(f124,plain,(
% 12.83/2.09 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((cP_1 @ (f @ a) @ X2))) | ($true != ((cP_1 @ (f @ b) @ X1))) | ($true != ((cP_1 @ (f @ c) @ X0))) | ($true = ((cQ_2 @ X2 @ X1 @ X0)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f121])).
% 12.83/2.09 thf(f127,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true != $true) | ($true != ((cP_2 @ (f @ X2) @ X3))) | (((cP_2 @ (f @ X1) @ X4)) != $true) | ($true != ((cP_2 @ (f @ X0) @ X5))) | ($true = ((cQ_3 @ X5 @ X4 @ X3))) | (((cQ_2 @ X0 @ X1 @ X2)) = $false)) )),
% 12.83/2.09 inference(constrained_superposition,[],[f18,f45])).
% 12.83/2.09 thf(f128,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true != ((cP_2 @ (f @ X2) @ X3))) | (((cP_2 @ (f @ X1) @ X4)) != $true) | ($true != ((cP_2 @ (f @ X0) @ X5))) | ($true = ((cQ_3 @ X5 @ X4 @ X3))) | (((cQ_2 @ X0 @ X1 @ X2)) = $false)) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f127])).
% 12.83/2.09 thf(f133,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true != $true) | ($true != ((cP_3 @ (f @ X2) @ X3))) | (((cP_3 @ (f @ X1) @ X4)) != $true) | ($true != ((cP_3 @ (f @ X0) @ X5))) | ($true = ((cQ_4 @ X5 @ X4 @ X3))) | (((cQ_3 @ X0 @ X1 @ X2)) = $false)) )),
% 12.83/2.09 inference(constrained_superposition,[],[f24,f45])).
% 12.83/2.09 thf(f134,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true != ((cP_3 @ (f @ X2) @ X3))) | (((cP_3 @ (f @ X1) @ X4)) != $true) | ($true != ((cP_3 @ (f @ X0) @ X5))) | ($true = ((cQ_4 @ X5 @ X4 @ X3))) | (((cQ_3 @ X0 @ X1 @ X2)) = $false)) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f133])).
% 12.83/2.09 thf(f135,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true != $true) | ($true != ((cP_4 @ (f @ X2) @ X3))) | (((cP_4 @ (f @ X1) @ X4)) != $true) | ($true != ((cP_4 @ (f @ X0) @ X5))) | ($true = ((cQ_5 @ X5 @ X4 @ X3))) | (((cQ_4 @ X0 @ X1 @ X2)) = $false)) )),
% 12.83/2.09 inference(constrained_superposition,[],[f30,f45])).
% 12.83/2.09 thf(f136,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true != ((cP_4 @ (f @ X2) @ X3))) | (((cP_4 @ (f @ X1) @ X4)) != $true) | ($true != ((cP_4 @ (f @ X0) @ X5))) | ($true = ((cQ_5 @ X5 @ X4 @ X3))) | (((cQ_4 @ X0 @ X1 @ X2)) = $false)) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f135])).
% 12.83/2.09 thf(f137,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true != $true) | ($true != ((cP_5 @ (f @ X2) @ X3))) | (((cP_5 @ (f @ X1) @ X4)) != $true) | ($true != ((cP_5 @ (f @ X0) @ X5))) | ($true = ((cQ_6 @ X5 @ X4 @ X3))) | (((cQ_5 @ X0 @ X1 @ X2)) = $false)) )),
% 12.83/2.09 inference(constrained_superposition,[],[f36,f45])).
% 12.83/2.09 thf(f138,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true != ((cP_5 @ (f @ X2) @ X3))) | (((cP_5 @ (f @ X1) @ X4)) != $true) | ($true != ((cP_5 @ (f @ X0) @ X5))) | ($true = ((cQ_6 @ X5 @ X4 @ X3))) | (((cQ_5 @ X0 @ X1 @ X2)) = $false)) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f137])).
% 12.83/2.09 thf(f139,plain,(
% 12.83/2.09 ( ! [X3 : $i,X8 : $i,X6 : $i,X7 : $i,X4 : $i,X5 : $i] : ((((cQ_6 @ X3 @ X4 @ X5)) != $true) | (((cP_6 @ (f @ X4) @ X7)) != $true) | (((cP_6 @ (f @ X3) @ X6)) != $true) | (((cP_6 @ (f @ X5) @ X8)) != $true)) )),
% 12.83/2.09 inference(forward_subsumption_resolution,[],[f42,f43])).
% 12.83/2.09 thf(f140,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true != $true) | ($true != ((cP_6 @ (f @ X1) @ X3))) | ($true != ((cP_6 @ (f @ X0) @ X4))) | (((cP_6 @ (f @ X2) @ X5)) != $true) | (((cQ_6 @ X0 @ X1 @ X2)) = $false)) )),
% 12.83/2.09 inference(constrained_superposition,[],[f139,f45])).
% 12.83/2.09 thf(f141,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true != ((cP_6 @ (f @ X1) @ X3))) | ($true != ((cP_6 @ (f @ X0) @ X4))) | (((cP_6 @ (f @ X2) @ X5)) != $true) | (((cQ_6 @ X0 @ X1 @ X2)) = $false)) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f140])).
% 12.83/2.09 thf(f202,plain,(
% 12.83/2.09 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true != ((cP_1 @ (f @ b) @ X0))) | ($true != ((cP_1 @ (f @ c) @ X1))) | ($true = ((cQ_2 @ a @ X0 @ X1)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f124,f50])).
% 12.83/2.09 thf(f205,plain,(
% 12.83/2.09 ( ! [X0 : $i,X1 : $i] : (($true != ((cP_1 @ (f @ b) @ X0))) | ($true != ((cP_1 @ (f @ c) @ X1))) | ($true = ((cQ_2 @ a @ X0 @ X1)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f202])).
% 12.83/2.09 thf(f210,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((cP_6 @ (f @ X0) @ X1)) != $true) | ($true != ((cP_6 @ (f @ X2) @ X3))) | ($false = ((cQ_6 @ X0 @ b @ X2)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f141,f97])).
% 12.83/2.09 thf(f215,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((cP_6 @ (f @ X2) @ X3))) | (((cP_6 @ (f @ X0) @ X1)) != $true) | ($false = ((cQ_6 @ X0 @ b @ X2)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f210])).
% 12.83/2.09 thf(f247,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((cP_2 @ (f @ X0) @ X1)) != $true) | ($true != ((cP_2 @ (f @ X2) @ X3))) | ($true = ((cQ_3 @ X3 @ X1 @ c))) | ($false = ((cQ_2 @ X2 @ X0 @ c)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f128,f60])).
% 12.83/2.09 thf(f260,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((cP_2 @ (f @ X2) @ X3))) | (((cP_2 @ (f @ X0) @ X1)) != $true) | ($true = ((cQ_3 @ X3 @ X1 @ c))) | ($false = ((cQ_2 @ X2 @ X0 @ c)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f247])).
% 12.83/2.09 thf(f265,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((cP_3 @ (f @ X0) @ X1)) != $true) | ($true != ((cP_3 @ (f @ X2) @ X3))) | ($true = ((cQ_4 @ X3 @ X1 @ c))) | ($false = ((cQ_3 @ X2 @ X0 @ c)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f134,f68])).
% 12.83/2.09 thf(f272,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((cP_3 @ (f @ X2) @ X3))) | (((cP_3 @ (f @ X0) @ X1)) != $true) | ($true = ((cQ_4 @ X3 @ X1 @ c))) | ($false = ((cQ_3 @ X2 @ X0 @ c)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f265])).
% 12.83/2.09 thf(f281,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((cP_4 @ (f @ X0) @ X1)) != $true) | ($true != ((cP_4 @ (f @ X2) @ X3))) | ($true = ((cQ_5 @ X3 @ X1 @ c))) | ($false = ((cQ_4 @ X2 @ X0 @ c)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f136,f76])).
% 12.83/2.09 thf(f288,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((cP_4 @ (f @ X2) @ X3))) | (((cP_4 @ (f @ X0) @ X1)) != $true) | ($true = ((cQ_5 @ X3 @ X1 @ c))) | ($false = ((cQ_4 @ X2 @ X0 @ c)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f281])).
% 12.83/2.09 thf(f297,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((cP_5 @ (f @ X0) @ X1)) != $true) | ($true != ((cP_5 @ (f @ X2) @ X3))) | ($true = ((cQ_6 @ X3 @ X1 @ c))) | ($false = ((cQ_5 @ X2 @ X0 @ c)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f138,f84])).
% 12.83/2.09 thf(f304,plain,(
% 12.83/2.09 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((cP_5 @ (f @ X2) @ X3))) | (((cP_5 @ (f @ X0) @ X1)) != $true) | ($true = ((cQ_6 @ X3 @ X1 @ c))) | ($false = ((cQ_5 @ X2 @ X0 @ c)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f297])).
% 12.83/2.09 thf(f396,plain,(
% 12.83/2.09 ( ! [X0 : $i] : (($true != $true) | ($true != ((cP_1 @ (f @ c) @ X0))) | ($true = ((cQ_2 @ a @ b @ X0)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f205,f51])).
% 12.83/2.09 thf(f399,plain,(
% 12.83/2.09 ( ! [X0 : $i] : (($true != ((cP_1 @ (f @ c) @ X0))) | ($true = ((cQ_2 @ a @ b @ X0)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f396])).
% 12.83/2.09 thf(f427,plain,(
% 12.83/2.09 ( ! [X0 : $i,X1 : $i] : (($true != $true) | (((cP_6 @ (f @ X0) @ X1)) != $true) | ($false = ((cQ_6 @ X0 @ b @ c)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f215,f98])).
% 12.83/2.09 thf(f440,plain,(
% 12.83/2.09 ( ! [X0 : $i,X1 : $i] : ((((cP_6 @ (f @ X0) @ X1)) != $true) | ($false = ((cQ_6 @ X0 @ b @ c)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f427])).
% 12.83/2.09 thf(f764,plain,(
% 12.83/2.09 ( ! [X0 : $i,X1 : $i] : (($true != $true) | (((cP_2 @ (f @ X0) @ X1)) != $true) | ($true = ((cQ_3 @ a @ X1 @ c))) | ($false = ((cQ_2 @ a @ X0 @ c)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f260,f58])).
% 12.83/2.09 thf(f771,plain,(
% 12.83/2.09 ( ! [X0 : $i,X1 : $i] : ((((cP_2 @ (f @ X0) @ X1)) != $true) | ($true = ((cQ_3 @ a @ X1 @ c))) | ($false = ((cQ_2 @ a @ X0 @ c)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f764])).
% 12.83/2.09 thf(f865,plain,(
% 12.83/2.09 ( ! [X0 : $i,X1 : $i] : (($true != $true) | (((cP_3 @ (f @ X0) @ X1)) != $true) | ($true = ((cQ_4 @ a @ X1 @ c))) | ($false = ((cQ_3 @ a @ X0 @ c)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f272,f66])).
% 12.83/2.09 thf(f870,plain,(
% 12.83/2.09 ( ! [X0 : $i,X1 : $i] : ((((cP_3 @ (f @ X0) @ X1)) != $true) | ($true = ((cQ_4 @ a @ X1 @ c))) | ($false = ((cQ_3 @ a @ X0 @ c)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f865])).
% 12.83/2.09 thf(f1009,plain,(
% 12.83/2.09 ( ! [X0 : $i,X1 : $i] : (($true != $true) | (((cP_4 @ (f @ X0) @ X1)) != $true) | ($true = ((cQ_5 @ a @ X1 @ c))) | ($false = ((cQ_4 @ a @ X0 @ c)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f288,f74])).
% 12.83/2.09 thf(f1016,plain,(
% 12.83/2.09 ( ! [X0 : $i,X1 : $i] : ((((cP_4 @ (f @ X0) @ X1)) != $true) | ($true = ((cQ_5 @ a @ X1 @ c))) | ($false = ((cQ_4 @ a @ X0 @ c)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f1009])).
% 12.83/2.09 thf(f1137,plain,(
% 12.83/2.09 ( ! [X0 : $i,X1 : $i] : (($true != $true) | (((cP_5 @ (f @ X0) @ X1)) != $true) | ($true = ((cQ_6 @ a @ X1 @ c))) | ($false = ((cQ_5 @ a @ X0 @ c)))) )),
% 12.83/2.09 inference(constrained_superposition,[],[f304,f82])).
% 12.83/2.09 thf(f1142,plain,(
% 12.83/2.09 ( ! [X0 : $i,X1 : $i] : ((((cP_5 @ (f @ X0) @ X1)) != $true) | ($true = ((cQ_6 @ a @ X1 @ c))) | ($false = ((cQ_5 @ a @ X0 @ c)))) )),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f1137])).
% 12.83/2.09 thf(f1762,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cQ_2 @ a @ b @ c)))),
% 12.83/2.09 inference(constrained_superposition,[],[f399,f52])).
% 12.83/2.09 thf(f1765,plain,(
% 12.83/2.09 ($true = ((cQ_2 @ a @ b @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f1762])).
% 12.83/2.09 thf(f1982,plain,(
% 12.83/2.09 ($true != $true) | ($false = ((cQ_6 @ a @ b @ c)))),
% 12.83/2.09 inference(constrained_superposition,[],[f440,f96])).
% 12.83/2.09 thf(f1989,plain,(
% 12.83/2.09 ($false = ((cQ_6 @ a @ b @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f1982])).
% 12.83/2.09 thf(f7018,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cQ_3 @ a @ b @ c))) | ($false = ((cQ_2 @ a @ b @ c)))),
% 12.83/2.09 inference(constrained_superposition,[],[f771,f59])).
% 12.83/2.09 thf(f7033,plain,(
% 12.83/2.09 ($true = ((cQ_3 @ a @ b @ c))) | ($false = ((cQ_2 @ a @ b @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f7018])).
% 12.83/2.09 thf(f7072,definition,(
% 12.83/2.09 spl0_458 <=> ($true = ((cQ_3 @ a @ b @ c)))),
% 12.83/2.09 introduced(definition,[new_symbols(definition,[spl0_458])],[avatar_definition])).
% 12.83/2.09 thf(f7074,plain,(
% 12.83/2.09 ($true = ((cQ_3 @ a @ b @ c))) | ~spl0_458),
% 12.83/2.09 inference(avatar_component_clause,[],[f7072])).
% 12.83/2.09 thf(f7082,definition,(
% 12.83/2.09 spl0_460 <=> ($false = ((cQ_2 @ a @ b @ c)))),
% 12.83/2.09 introduced(definition,[new_symbols(definition,[spl0_460])],[avatar_definition])).
% 12.83/2.09 thf(f7084,plain,(
% 12.83/2.09 ($false = ((cQ_2 @ a @ b @ c))) | ~spl0_460),
% 12.83/2.09 inference(avatar_component_clause,[],[f7082])).
% 12.83/2.09 thf(f7085,plain,(
% 12.83/2.09 spl0_460 | spl0_458),
% 12.83/2.09 inference(avatar_split_clause,[],[f7033,f7072,f7082])).
% 12.83/2.09 thf(f8780,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cQ_4 @ a @ b @ c))) | ($false = ((cQ_3 @ a @ b @ c)))),
% 12.83/2.09 inference(constrained_superposition,[],[f870,f67])).
% 12.83/2.09 thf(f8793,plain,(
% 12.83/2.09 ($true = ((cQ_4 @ a @ b @ c))) | ($false = ((cQ_3 @ a @ b @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f8780])).
% 12.83/2.09 thf(f8827,definition,(
% 12.83/2.09 spl0_721 <=> ($true = ((cQ_4 @ a @ b @ c)))),
% 12.83/2.09 introduced(definition,[new_symbols(definition,[spl0_721])],[avatar_definition])).
% 12.83/2.09 thf(f8829,plain,(
% 12.83/2.09 ($true = ((cQ_4 @ a @ b @ c))) | ~spl0_721),
% 12.83/2.09 inference(avatar_component_clause,[],[f8827])).
% 12.83/2.09 thf(f8837,definition,(
% 12.83/2.09 spl0_723 <=> ($false = ((cQ_3 @ a @ b @ c)))),
% 12.83/2.09 introduced(definition,[new_symbols(definition,[spl0_723])],[avatar_definition])).
% 12.83/2.09 thf(f8839,plain,(
% 12.83/2.09 ($false = ((cQ_3 @ a @ b @ c))) | ~spl0_723),
% 12.83/2.09 inference(avatar_component_clause,[],[f8837])).
% 12.83/2.09 thf(f8840,plain,(
% 12.83/2.09 spl0_723 | spl0_721),
% 12.83/2.09 inference(avatar_split_clause,[],[f8793,f8827,f8837])).
% 12.83/2.09 thf(f10489,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cQ_5 @ a @ b @ c))) | ($false = ((cQ_4 @ a @ b @ c)))),
% 12.83/2.09 inference(constrained_superposition,[],[f1016,f75])).
% 12.83/2.09 thf(f10502,plain,(
% 12.83/2.09 ($true = ((cQ_5 @ a @ b @ c))) | ($false = ((cQ_4 @ a @ b @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f10489])).
% 12.83/2.09 thf(f10536,definition,(
% 12.83/2.09 spl0_977 <=> ($true = ((cQ_5 @ a @ b @ c)))),
% 12.83/2.09 introduced(definition,[new_symbols(definition,[spl0_977])],[avatar_definition])).
% 12.83/2.09 thf(f10538,plain,(
% 12.83/2.09 ($true = ((cQ_5 @ a @ b @ c))) | ~spl0_977),
% 12.83/2.09 inference(avatar_component_clause,[],[f10536])).
% 12.83/2.09 thf(f10546,definition,(
% 12.83/2.09 spl0_979 <=> ($false = ((cQ_4 @ a @ b @ c)))),
% 12.83/2.09 introduced(definition,[new_symbols(definition,[spl0_979])],[avatar_definition])).
% 12.83/2.09 thf(f10548,plain,(
% 12.83/2.09 ($false = ((cQ_4 @ a @ b @ c))) | ~spl0_979),
% 12.83/2.09 inference(avatar_component_clause,[],[f10546])).
% 12.83/2.09 thf(f10549,plain,(
% 12.83/2.09 spl0_979 | spl0_977),
% 12.83/2.09 inference(avatar_split_clause,[],[f10502,f10536,f10546])).
% 12.83/2.09 thf(f11964,plain,(
% 12.83/2.09 ($true != $true) | ($true = ((cQ_6 @ a @ b @ c))) | ($false = ((cQ_5 @ a @ b @ c)))),
% 12.83/2.09 inference(constrained_superposition,[],[f1142,f83])).
% 12.83/2.09 thf(f11977,plain,(
% 12.83/2.09 ($true = ((cQ_6 @ a @ b @ c))) | ($false = ((cQ_5 @ a @ b @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f11964])).
% 12.83/2.09 thf(f11997,plain,(
% 12.83/2.09 ($true = $false) | ($false = ((cQ_5 @ a @ b @ c)))),
% 12.83/2.09 inference(forward_demodulation,[],[f11977,f1989])).
% 12.83/2.09 thf(f11998,plain,(
% 12.83/2.09 ($false = ((cQ_5 @ a @ b @ c)))),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f11997])).
% 12.83/2.09 thf(f34615,plain,(
% 12.83/2.09 ($true = $false) | ~spl0_977),
% 12.83/2.09 inference(constrained_superposition,[],[f11998,f10538])).
% 12.83/2.09 thf(f34625,plain,(
% 12.83/2.09 $false | ~spl0_977),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f34615])).
% 12.83/2.09 thf(f34626,plain,(
% 12.83/2.09 ~spl0_977),
% 12.83/2.09 inference(avatar_contradiction_clause,[],[f34625])).
% 12.83/2.09 thf(f34631,plain,(
% 12.83/2.09 ($true = $false) | (~spl0_721 | ~spl0_979)),
% 12.83/2.09 inference(constrained_superposition,[],[f10548,f8829])).
% 12.83/2.09 thf(f34641,plain,(
% 12.83/2.09 $false | (~spl0_721 | ~spl0_979)),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f34631])).
% 12.83/2.09 thf(f34642,plain,(
% 12.83/2.09 ~spl0_721 | ~spl0_979),
% 12.83/2.09 inference(avatar_contradiction_clause,[],[f34641])).
% 12.83/2.09 thf(f34647,plain,(
% 12.83/2.09 ($true = $false) | (~spl0_458 | ~spl0_723)),
% 12.83/2.09 inference(constrained_superposition,[],[f8839,f7074])).
% 12.83/2.09 thf(f34657,plain,(
% 12.83/2.09 $false | (~spl0_458 | ~spl0_723)),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f34647])).
% 12.83/2.09 thf(f34658,plain,(
% 12.83/2.09 ~spl0_458 | ~spl0_723),
% 12.83/2.09 inference(avatar_contradiction_clause,[],[f34657])).
% 12.83/2.09 thf(f34662,plain,(
% 12.83/2.09 ($true = $false) | ~spl0_460),
% 12.83/2.09 inference(constrained_superposition,[],[f7084,f1765])).
% 12.83/2.09 thf(f34669,plain,(
% 12.83/2.09 $false | ~spl0_460),
% 12.83/2.09 inference(trivial_inequality_removal,[],[f34662])).
% 12.83/2.09 thf(f34670,plain,(
% 12.83/2.09 ~spl0_460),
% 12.83/2.09 inference(avatar_contradiction_clause,[],[f34669])).
% 12.83/2.09 cnf(s363, plain, spl0_458 | spl0_460, inference(sat_conversion,[],[f7085])).
% 12.83/2.09 cnf(s562, plain, spl0_721 | spl0_723, inference(sat_conversion,[],[f8840])).
% 12.83/2.09 cnf(s754, plain, spl0_977 | spl0_979, inference(sat_conversion,[],[f10549])).
% 12.83/2.09 cnf(s2747, plain, ~spl0_977, inference(sat_conversion,[],[f34626])).
% 12.83/2.09 cnf(s2751, plain, ~spl0_721 | ~spl0_979, inference(sat_conversion,[],[f34642])).
% 12.83/2.09 cnf(s2755, plain, ~spl0_458 | ~spl0_723, inference(sat_conversion,[],[f34658])).
% 12.83/2.09 cnf(s2758, plain, ~spl0_460, inference(sat_conversion,[],[f34670])).
% 12.83/2.09 cnf(s3073, plain, spl0_979, inference(rat,[],[s754,s2747])).
% 12.83/2.09 cnf(s3075, plain, ~spl0_721, inference(rat,[],[s2751,s3073])).
% 12.83/2.09 cnf(s3447, plain, spl0_723, inference(rat,[],[s562,s3075])).
% 12.83/2.09 cnf(s3449, plain, ~spl0_458, inference(rat,[],[s2755,s3447])).
% 12.83/2.09 cnf(s3714, plain, $false, inference(rat,[],[s363,s2758,s3449])).
% 12.83/2.09 thf(f34671,plain,(
% 12.83/2.09 $false),
% 12.83/2.09 inference(avatar_sat_refutation,[],[s3714])).
% 12.83/2.09 % SZS output end Proof for theBenchmark
% 12.83/2.09 % (2919148)------------------------------
% 12.83/2.09 % (2919148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.83/2.09 % (2919148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.09 % (2919148)CaDiCaL version: 2.1.3
% 12.83/2.09 % (2919148)Termination reason: Refutation
% 12.83/2.09 % (2919148)Time elapsed: 1.827 s
% 12.83/2.09 % (2919148)Peak memory usage: 25 MB
% 12.83/2.09 % (2919148)Instructions burned: 4101 (million)
% 12.83/2.09 % (2919123)Success in time 1.873 s
% 12.83/2.09 % Vampire exiting
%------------------------------------------------------------------------------