%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : COM162^1 : TPTP v9.3.1. Released v7.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 07:46:28 AM UTC 2026
% Result : Theorem 7.74s 1.49s
% Output : Refutation 7.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM162^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 % Computer : n014.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 17:47:00 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 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
% 4.01/0.94 % (2987595)Will run a generic schedule for satisfiability detection.
% 4.01/0.94 % (2987605)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2009562241:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.01/0.94 % (2987601)% WARNING: option uhcvi not known.
% 4.01/0.94 % (2987604)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=655138433:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.01/0.94 % (2987600)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1497958998_2999 on theBenchmark for (2999ds/0Mi)
% 4.01/0.94 % (2987603)dis+10_1_sil=32000:sp=arity:random_seed=2448769050:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.01/0.94 % (2987606)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=847575262:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.01/0.94 % (2987602)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1590325923:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.01/0.94 % (2987601)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3843595186:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.01/0.94 % (2987604)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.01/0.94 % (2987601)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.01/0.94 % Exception at run slice level
% 4.01/0.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.01/0.94 % (2987601)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.01/0.94 % (2987605)Instruction limit reached!
% 4.01/0.94 % (2987605)------------------------------
% 4.01/0.94 % (2987605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.01/0.94 % (2987605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/0.94 % (2987605)CaDiCaL version: 2.1.3
% 4.01/0.94 % (2987605)Termination reason: Instruction limit
% 4.01/0.94 % (2987605)Termination phase: Saturation
% 4.01/0.94 % (2987605)Time elapsed: 0.041 s
% 4.01/0.94 % (2987605)Peak memory usage: 13 MB
% 4.01/0.94 % (2987605)Instructions burned: 133 (million)
% 4.01/0.94 % (2987615)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3055747462:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.01/0.94 % (2987603)Instruction limit reached!
% 4.01/0.94 % (2987603)------------------------------
% 4.01/0.94 % (2987603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.01/0.94 % (2987603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/0.94 % (2987603)CaDiCaL version: 2.1.3
% 4.01/0.94 % (2987603)Termination reason: Instruction limit
% 4.01/0.94 % (2987603)Termination phase: Saturation
% 4.01/0.94 % (2987603)Time elapsed: 0.047 s
% 4.01/0.94 % (2987603)Peak memory usage: 13 MB
% 4.01/0.94 % (2987603)Instructions burned: 103 (million)
% 4.01/0.94 % (2987604)Instruction limit reached!
% 4.01/0.94 % (2987604)------------------------------
% 4.01/0.94 % (2987604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.01/0.94 % (2987604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/0.94 % (2987604)CaDiCaL version: 2.1.3
% 4.01/0.94 % (2987604)Termination reason: Instruction limit
% 4.01/0.94 % (2987604)Termination phase: Saturation
% 4.01/0.94 % (2987604)Time elapsed: 0.056 s
% 4.01/0.94 % (2987604)Peak memory usage: 13 MB
% 4.01/0.94 % (2987604)Instructions burned: 117 (million)
% 4.01/0.94 % (2987614)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3392931964:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.01/0.94 % (2987617)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=720812156:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.01/0.94 % (2987606)Instruction limit reached!
% 4.01/0.94 % (2987606)------------------------------
% 4.01/0.94 % (2987606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.01/0.94 % (2987606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/0.94 % (2987606)CaDiCaL version: 2.1.3
% 4.01/0.94 % (2987606)Termination reason: Instruction limit
% 4.01/0.94 % (2987606)Termination phase: Saturation
% 4.01/0.94 % (2987606)Time elapsed: 0.074 s
% 4.01/0.94 % (2987606)Peak memory usage: 14 MB
% 4.01/0.94 % (2987606)Instructions burned: 160 (million)
% 7.74/1.49 % (2987618)ott-21_1_sil=16000:fs=off:random_seed=1442186376:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.74/1.49 % (2987615)Instruction limit reached!
% 7.74/1.49 % (2987615)------------------------------
% 7.74/1.49 % (2987615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.49 % (2987615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.49 % (2987615)CaDiCaL version: 2.1.3
% 7.74/1.49 % (2987615)Termination reason: Instruction limit
% 7.74/1.49 % (2987615)Termination phase: Saturation
% 7.74/1.49 % (2987615)Time elapsed: 0.035 s
% 7.74/1.49 % (2987615)Peak memory usage: 13 MB
% 7.74/1.49 % (2987615)Instructions burned: 133 (million)
% 7.74/1.49 % (2987617)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.74/1.49 % (2987623)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=650843837:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.74/1.49 % (2987622)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1723800528:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.74/1.49 % (2987617)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.74/1.49 % Exception at run slice level
% 7.74/1.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.74/1.49 % Exception at run slice level
% 7.74/1.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.74/1.49 % (2987626)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3091934281:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.74/1.49 % (2987627)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=639061982:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 7.74/1.49 % (2987618)Instruction limit reached!
% 7.74/1.49 % (2987618)------------------------------
% 7.74/1.49 % (2987618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.49 % (2987618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.49 % (2987618)CaDiCaL version: 2.1.3
% 7.74/1.49 % (2987618)Termination reason: Instruction limit
% 7.74/1.49 % (2987618)Termination phase: Saturation
% 7.74/1.49 % (2987618)Time elapsed: 0.080 s
% 7.74/1.49 % (2987618)Peak memory usage: 13 MB
% 7.74/1.49 % (2987618)Instructions burned: 181 (million)
% 7.74/1.49 % Exception at run slice level
% 7.74/1.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.74/1.49 % (2987630)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=3910311948: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)
% 7.74/1.49 % (2987631)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3443651408:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 7.74/1.49 % (2987630)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.74/1.49 % (2987631)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.74/1.49 % (2987622)Instruction limit reached!
% 7.74/1.49 % (2987622)------------------------------
% 7.74/1.49 % (2987622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.49 % (2987622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.49 % (2987622)CaDiCaL version: 2.1.3
% 7.74/1.49 % (2987622)Termination reason: Instruction limit
% 7.74/1.49 % (2987622)Termination phase: Saturation
% 7.74/1.49 % (2987622)Time elapsed: 0.224 s
% 7.74/1.49 % (2987622)Peak memory usage: 14 MB
% 7.74/1.49 % (2987622)Instructions burned: 479 (million)
% 7.74/1.49 % (2987634)fmb+10_1_sil=64000:random_seed=1020082343:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 7.74/1.49 % (2987634)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 7.74/1.49 % Exception at run slice level
% 7.74/1.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.74/1.49 % (2987636)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4101433231:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 7.74/1.49 % (2987617)Instruction limit reached!
% 7.74/1.49 % (2987617)------------------------------
% 7.74/1.49 % (2987617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.49 % (2987617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.49 % (2987617)CaDiCaL version: 2.1.3
% 7.74/1.49 % (2987617)Termination reason: Instruction limit
% 7.74/1.49 % (2987617)Termination phase: Saturation
% 7.74/1.49 % (2987617)Time elapsed: 0.320 s
% 7.74/1.49 % (2987617)Peak memory usage: 15 MB
% 7.74/1.49 % (2987617)Instructions burned: 686 (million)
% 7.74/1.49 % (2987638)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3764587724:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 7.74/1.49 % Exception at run slice level
% 7.74/1.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.74/1.49 % (2987626)Instruction limit reached!
% 7.74/1.49 % (2987626)------------------------------
% 7.74/1.49 % (2987626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.49 % (2987626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.49 % (2987626)CaDiCaL version: 2.1.3
% 7.74/1.49 % (2987626)Termination reason: Instruction limit
% 7.74/1.49 % (2987626)Termination phase: Saturation
% 7.74/1.49 % (2987626)Time elapsed: 0.299 s
% 7.74/1.49 % (2987626)Peak memory usage: 18 MB
% 7.74/1.49 % (2987626)Instructions burned: 1183 (million)
% 7.74/1.49 % (2987641)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4088166835:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 7.74/1.49 % (2987640)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3713485877:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 7.74/1.49 % Exception at run slice level
% 7.74/1.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.74/1.49 % (2987640)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.74/1.49 % (2987641)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 7.74/1.49 % (2987641)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.74/1.49 % (2987644)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=993051654:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 7.74/1.49 % Exception at run slice level
% 7.74/1.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.74/1.49 % (2987646)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2938827683:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 7.74/1.49 % (2987630)Instruction limit reached!
% 7.74/1.49 % (2987630)------------------------------
% 7.74/1.49 % (2987630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.49 % (2987630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.49 % (2987630)CaDiCaL version: 2.1.3
% 7.74/1.49 % (2987630)Termination reason: Instruction limit
% 7.74/1.49 % (2987630)Termination phase: Saturation
% 7.74/1.49 % (2987630)Time elapsed: 0.339 s
% 7.74/1.49 % (2987630)Peak memory usage: 16 MB
% 7.74/1.49 % (2987630)Instructions burned: 692 (million)
% 7.74/1.49 % Exception at run slice level
% 7.74/1.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.74/1.49 % (2987648)ott-2_1_sil=16000:newcnf=on:random_seed=3831498790:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 7.74/1.49 % (2987649)ott+10_1_sil=32000:tgt=ground:random_seed=603457015:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi)
% 7.74/1.49 % (2987648)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.74/1.49 % (2987631)Instruction limit reached!
% 7.74/1.49 % (2987631)------------------------------
% 7.74/1.49 % (2987631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.49 % (2987631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.49 % (2987631)CaDiCaL version: 2.1.3
% 7.74/1.49 % (2987631)Termination reason: Instruction limit
% 7.74/1.49 % (2987631)Termination phase: Saturation
% 7.74/1.49 % (2987631)Time elapsed: 0.420 s
% 7.74/1.49 % (2987631)Peak memory usage: 18 MB
% 7.74/1.49 % (2987631)Instructions burned: 879 (million)
% 7.74/1.49 % (2987652)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1849139840:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 7.74/1.49 % Exception at run slice level
% 7.74/1.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.74/1.49 % (2987654)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1590847913:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 7.74/1.49 % (2987654)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.74/1.49 % (2987648)Instruction limit reached!
% 7.74/1.49 % (2987648)------------------------------
% 7.74/1.49 % (2987648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.49 % (2987648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.49 % (2987648)CaDiCaL version: 2.1.3
% 7.74/1.49 % (2987648)Termination reason: Instruction limit
% 7.74/1.49 % (2987648)Termination phase: Saturation
% 7.74/1.49 % (2987648)Time elapsed: 0.401 s
% 7.74/1.49 % (2987648)Peak memory usage: 16 MB
% 7.74/1.49 % (2987648)Instructions burned: 870 (million)
% 7.74/1.49 % (2987641)Instruction limit reached!
% 7.74/1.49 % (2987641)------------------------------
% 7.74/1.49 % (2987641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.49 % (2987641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.49 % (2987641)CaDiCaL version: 2.1.3
% 7.74/1.49 % (2987641)Termination reason: Instruction limit
% 7.74/1.49 % (2987641)Termination phase: Saturation
% 7.74/1.49 % (2987641)Time elapsed: 0.507 s
% 7.74/1.49 % (2987641)Peak memory usage: 19 MB
% 7.74/1.49 % (2987641)Instructions burned: 1473 (million)
% 7.74/1.49 % (2987656)dis+21_1_sil=32000:sas=cadical:random_seed=89294515:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 7.74/1.49 % (2987657)ott+11_1_sil=16000:gs=on:random_seed=3256115135:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2990 on theBenchmark for (2990ds/2251Mi)
% 7.74/1.49 % (2987657)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.74/1.49 % (2987601) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2987595-2987601"...
% 7.74/1.49 % (2987601)...printing done.
% 7.74/1.49 % (2987601)Refutation found. Thanks to Tanya!
% 7.74/1.49 % SZS status Theorem for theBenchmark
% 7.74/1.49 % SZS output start Proof for theBenchmark
% 7.74/1.49 thf(type_def_5, type, binDag_Mirabelle_dag: $tType).
% 7.74/1.49 thf(type_def_6, type, tuple_isomorphism: ($tType * $tType * $tType) > $tType).
% 7.74/1.49 thf(type_def_7, type, code_natural: $tType).
% 7.74/1.49 thf(type_def_8, type, code_term: $tType).
% 7.74/1.49 thf(type_def_9, type, product_unit: $tType).
% 7.74/1.49 thf(type_def_10, type, product_prod: ($tType * $tType) > $tType).
% 7.74/1.49 thf(type_def_11, type, typerep: $tType).
% 7.74/1.49 thf(type_def_12, type, simpl_ref: $tType).
% 7.74/1.49 thf(type_def_13, type, literal: $tType).
% 7.74/1.49 thf(type_def_14, type, sum_sum: ($tType * $tType) > $tType).
% 7.74/1.49 thf(type_def_15, type, option: $tType > $tType).
% 7.74/1.49 thf(type_def_16, type, list: $tType > $tType).
% 7.74/1.49 thf(type_def_17, type, set: $tType > $tType).
% 7.74/1.49 thf(type_def_18, type, num: $tType).
% 7.74/1.49 thf(type_def_19, type, nat: $tType).
% 7.74/1.49 thf(type_def_20, type, itself: $tType > $tType).
% 7.74/1.49 thf(type_def_21, type, sTfun: ($tType * $tType) > $tType).
% 7.74/1.49 thf(func_def_0, type, enum: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_1, type, typerep2: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_2, type, type: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_3, type, cl_HOL_Oequal: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_4, type, code_term_of: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_5, type, size: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_6, type, one: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_7, type, zero: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_8, type, numeral: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_9, type, field: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_10, type, neg_numeral: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_11, type, group_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_12, type, monoid_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_13, type, zero_neq_one: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_14, type, semiring_char_0: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_15, type, semiring_div: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_16, type, division_ring: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_17, type, semigroup_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_18, type, semidom_divide: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_19, type, comm_semiring_1: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_20, type, comm_monoid_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_21, type, linordered_field: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_22, type, ab_semigroup_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_23, type, quickcheck_random: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_24, type, semiring_div_parity: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_25, type, cancel_semigroup_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_26, type, cancel1352612707id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_27, type, linord219039673up_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_28, type, ordere779506340up_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_29, type, canoni770627133id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_30, type, semiri456707255roduct: !>[X0: $tType]:((itself @ X0 > $o))).
% 7.74/1.49 thf(func_def_31, type, bNF_Greatest_Shift: !>[X0: $tType]:((set @ list @ X0 > X0 > set @ list @ X0))).
% 7.74/1.49 thf(func_def_32, type, basic_BNF_size_sum: !>[X0: $tType, X1: $tType]:(((X0 > nat) > (X1 > nat) > sum_sum @ X0 @ X1 > nat))).
% 7.74/1.49 thf(func_def_33, type, binDag476092410e_Node: (binDag_Mirabelle_dag > simpl_ref > binDag_Mirabelle_dag > binDag_Mirabelle_dag)).
% 7.74/1.49 thf(func_def_34, type, binDag_Mirabelle_Tip: binDag_Mirabelle_dag).
% 7.74/1.49 thf(func_def_35, type, binDag1297733282se_dag: !>[X0: $tType]:((X0 > (binDag_Mirabelle_dag > simpl_ref > binDag_Mirabelle_dag > X0) > binDag_Mirabelle_dag > X0))).
% 7.74/1.49 thf(func_def_36, type, binDag1442713106ec_dag: !>[X0: $tType]:((X0 > (binDag_Mirabelle_dag > simpl_ref > binDag_Mirabelle_dag > X0 > X0 > X0) > binDag_Mirabelle_dag > X0))).
% 7.74/1.49 thf(func_def_37, type, binDag1924123185ze_dag: (binDag_Mirabelle_dag > nat)).
% 7.74/1.49 thf(func_def_38, type, code_Suc: (code_natural > code_natural)).
% 7.74/1.49 thf(func_def_39, type, code_case_natural: !>[X0: $tType]:((X0 > (code_natural > X0) > code_natural > X0))).
% 7.74/1.49 thf(func_def_40, type, code_rec_natural: !>[X0: $tType]:((X0 > (code_natural > X0 > X0) > code_natural > X0))).
% 7.74/1.49 thf(func_def_41, type, code_size_natural: (code_natural > nat)).
% 7.74/1.49 thf(func_def_42, type, one_one: !>[X0: $tType]:(X0)).
% 7.74/1.49 thf(func_def_43, type, plus_plus: !>[X0: $tType]:((X0 > X0 > X0))).
% 7.74/1.49 thf(func_def_44, type, zero_zero: !>[X0: $tType]:(X0)).
% 7.74/1.49 thf(func_def_45, type, size_bool: ($o > nat)).
% 7.74/1.49 thf(func_def_46, type, default_default: !>[X0: $tType]:(X0)).
% 7.74/1.49 thf(func_def_47, type, undefined: !>[X0: $tType]:(X0)).
% 7.74/1.49 thf(func_def_48, type, if: !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 7.74/1.49 thf(func_def_49, type, gen_length: !>[X0: $tType]:((nat > list @ X0 > nat))).
% 7.74/1.49 thf(func_def_50, type, cons: !>[X0: $tType]:((X0 > list @ X0 > list @ X0))).
% 7.74/1.49 thf(func_def_51, type, size_list: !>[X0: $tType]:(((X0 > nat) > list @ X0 > nat))).
% 7.74/1.49 thf(func_def_52, type, splice: !>[X0: $tType]:((list @ X0 > list @ X0 > list @ X0))).
% 7.74/1.49 thf(func_def_53, type, suc: (nat > nat)).
% 7.74/1.49 thf(func_def_54, type, size_size: !>[X0: $tType]:((X0 > nat))).
% 7.74/1.49 thf(func_def_55, type, inc: (num > num)).
% 7.74/1.49 thf(func_def_56, type, nat_of_num: (num > nat)).
% 7.74/1.49 thf(func_def_57, type, neg_numeral_dbl_inc: !>[X0: $tType]:((X0 > X0))).
% 7.74/1.49 thf(func_def_58, type, bit0: (num > num)).
% 7.74/1.49 thf(func_def_59, type, bit1: (num > num)).
% 7.74/1.49 thf(func_def_60, type, one2: num).
% 7.74/1.49 thf(func_def_61, type, size_num: (num > nat)).
% 7.74/1.49 thf(func_def_62, type, numeral_numeral: !>[X0: $tType]:((num > X0))).
% 7.74/1.49 thf(func_def_63, type, none: !>[X0: $tType]:(option @ X0)).
% 7.74/1.49 thf(func_def_64, type, some: !>[X0: $tType]:((X0 > option @ X0))).
% 7.74/1.49 thf(func_def_65, type, case_option: !>[X0: $tType, X1: $tType]:((X0 > (X1 > X0) > option @ X1 > X0))).
% 7.74/1.49 thf(func_def_66, type, size_option: !>[X0: $tType]:(((X0 > nat) > option @ X0 > nat))).
% 7.74/1.49 thf(func_def_67, type, the: !>[X0: $tType]:((option @ X0 > X0))).
% 7.74/1.49 thf(func_def_68, type, product_Unity: product_unit).
% 7.74/1.49 thf(func_def_69, type, product_rec_bool: !>[X0: $tType]:((X0 > X0 > $o > X0))).
% 7.74/1.49 thf(func_def_70, type, product_rec_unit: !>[X0: $tType]:((X0 > product_unit > X0))).
% 7.74/1.49 thf(func_def_71, type, product_case_unit: !>[X0: $tType]:((X0 > product_unit > X0))).
% 7.74/1.49 thf(func_def_72, type, product_size_unit: (product_unit > nat)).
% 7.74/1.49 thf(func_def_73, type, type2: !>[X0: $tType]:(itself @ X0)).
% 7.74/1.49 thf(func_def_74, type, tuple_742722141rphism: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > product_prod @ X1 @ X2) > (product_prod @ X1 @ X2 > X0) > tuple_isomorphism @ X0 @ X1 @ X2))).
% 7.74/1.49 thf(func_def_75, type, tuple_1907371454rphism: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > nat) > (X1 > nat) > (X2 > nat) > tuple_isomorphism @ X0 @ X1 @ X2 > nat))).
% 7.74/1.49 thf(func_def_76, type, divide_divide: !>[X0: $tType]:((X0 > X0 > X0))).
% 7.74/1.49 thf(func_def_77, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 7.74/1.49 thf(func_def_78, type, sum_Inl: !>[X0: $tType, X1: $tType]:((X0 > sum_sum @ X0 @ X1))).
% 7.74/1.49 thf(func_def_79, type, sum_Inr: !>[X0: $tType, X1: $tType]:((X0 > sum_sum @ X1 @ X0))).
% 7.74/1.49 thf(func_def_80, type, transitive_ntrancl: !>[X0: $tType]:((nat > set @ product_prod @ X0 @ X0 > set @ product_prod @ X0 @ X0))).
% 7.74/1.49 thf(func_def_81, type, typerep3: (literal > list @ typerep > typerep)).
% 7.74/1.49 thf(func_def_82, type, size_typerep: (typerep > nat)).
% 7.74/1.49 thf(func_def_83, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 7.74/1.49 thf(func_def_84, type, a: simpl_ref).
% 7.74/1.49 thf(func_def_85, type, lt: binDag_Mirabelle_dag).
% 7.74/1.49 thf(func_def_86, type, rt: binDag_Mirabelle_dag).
% 7.74/1.49 thf(func_def_88, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 7.74/1.49 thf(func_def_89, type, vAND: ($o > $o > $o)).
% 7.74/1.49 thf(func_def_92, type, db2: !>[X0: $tType]:(X0)).
% 7.74/1.49 thf(func_def_93, type, db1: !>[X0: $tType]:(X0)).
% 7.74/1.49 thf(func_def_94, type, db0: !>[X0: $tType]:(X0)).
% 7.74/1.49 thf(func_def_95, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 7.74/1.49 thf(func_def_96, type, vOR: ($o > $o > $o)).
% 7.74/1.49 thf(func_def_97, type, vNOT: ($o > $o)).
% 7.74/1.49 thf(func_def_98, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 7.74/1.49 thf(func_def_99, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 7.74/1.49 thf(func_def_100, type, vIMP: ($o > $o > $o)).
% 7.74/1.49 thf(func_def_101, type, sP0: !>[X0: $tType, X1: $tType]:(((option @ X1 > option @ X0 > $o) > option @ X1 > option @ X0 > $o))).
% 7.74/1.49 thf(func_def_102, type, sK1: ((binDag_Mirabelle_dag > $o) > binDag_Mirabelle_dag)).
% 7.74/1.49 thf(func_def_103, type, sK2: ((binDag_Mirabelle_dag > $o) > simpl_ref)).
% 7.74/1.49 thf(func_def_104, type, sK3: ((binDag_Mirabelle_dag > $o) > binDag_Mirabelle_dag)).
% 7.74/1.49 thf(func_def_105, type, sK4: (binDag_Mirabelle_dag > binDag_Mirabelle_dag)).
% 7.74/1.49 thf(func_def_106, type, sK5: (binDag_Mirabelle_dag > simpl_ref)).
% 7.74/1.49 thf(func_def_107, type, sK6: (binDag_Mirabelle_dag > binDag_Mirabelle_dag)).
% 7.74/1.49 thf(func_def_108, type, sK7: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 7.74/1.49 thf(func_def_109, type, sK8: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 7.74/1.49 thf(func_def_110, type, sK9: ((nat > $o) > nat)).
% 7.74/1.49 thf(func_def_111, type, sK10: ((nat > nat > $o) > nat)).
% 7.74/1.49 thf(func_def_112, type, sK11: ((nat > nat > $o) > nat)).
% 7.74/1.49 thf(func_def_113, type, sK12: ((nat > nat > $o) > nat)).
% 7.74/1.49 thf(func_def_114, type, sK13: ((nat > nat > $o) > nat)).
% 7.74/1.49 thf(func_def_115, type, sK14: ((nat > $o) > nat)).
% 7.74/1.49 thf(func_def_116, type, sK15: (nat > nat)).
% 7.74/1.49 thf(func_def_117, type, sK16: ((nat > $o) > nat)).
% 7.74/1.49 thf(func_def_118, type, sK17: (nat > nat)).
% 7.74/1.49 thf(func_def_119, type, sK18: !>[X0: $tType]:(((nat > X0 > X0 > $o) > (nat > X0 > $o) > nat > X0))).
% 7.74/1.49 thf(func_def_120, type, sK19: !>[X0: $tType]:(((nat > X0 > X0 > $o) > (nat > X0 > $o) > X0))).
% 7.74/1.49 thf(func_def_121, type, sK20: !>[X0: $tType]:(((nat > X0 > X0 > $o) > (nat > X0 > $o) > nat))).
% 7.74/1.49 thf(func_def_122, type, sK21: ((code_natural > $o) > code_natural)).
% 7.74/1.49 thf(func_def_123, type, sK22: (code_natural > code_natural)).
% 7.74/1.49 thf(func_def_124, type, sK23: ((code_natural > code_natural > $o) > code_natural)).
% 7.74/1.49 thf(func_def_125, type, sK24: ((code_natural > code_natural > $o) > code_natural)).
% 7.74/1.49 thf(func_def_126, type, sK25: ((code_natural > code_natural > $o) > code_natural)).
% 7.74/1.49 thf(func_def_127, type, sK26: !>[X0: $tType]:(((code_natural > X0) > (code_natural > X0) > code_natural))).
% 7.74/1.49 thf(func_def_128, type, sK27: !>[X0: $tType, X1: $tType, X2: $tType]:(($o > (sum_sum @ X0 @ X1 > X2) > X2 > X1))).
% 7.74/1.49 thf(func_def_129, type, sK28: !>[X0: $tType, X1: $tType, X2: $tType]:(($o > (sum_sum @ X0 @ X1 > X2) > X2 > X0))).
% 7.74/1.49 thf(func_def_130, type, sK29: !>[X0: $tType]:((option @ X0 > X0))).
% 7.74/1.49 thf(func_def_131, type, sK30: !>[X0: $tType]:(((option @ X0 > $o) > X0))).
% 7.74/1.49 thf(func_def_132, type, sK31: !>[X0: $tType, X1: $tType]:(((option @ X1 > option @ X0 > $o) > option @ X1 > option @ X0 > X1))).
% 7.74/1.49 thf(func_def_133, type, sK32: !>[X0: $tType, X1: $tType]:(((option @ X1 > option @ X0 > $o) > option @ X1 > option @ X0 > X0))).
% 7.74/1.49 thf(func_def_134, type, sK33: !>[X0: $tType]:((option @ X0 > (X0 > $o) > X0))).
% 7.74/1.49 thf(func_def_135, type, sK34: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X0 > $o) > (X1 > $o) > X1))).
% 7.74/1.49 thf(func_def_136, type, sK35: !>[X0: $tType]:((nat > list @ X0 > list @ X0))).
% 7.74/1.49 thf(func_def_137, type, sK36: !>[X0: $tType]:((nat > list @ X0 > X0))).
% 7.74/1.49 thf(func_def_138, type, sK37: !>[X0: $tType]:((list @ X0 > nat > list @ X0))).
% 7.74/1.49 thf(func_def_139, type, sK38: !>[X0: $tType]:((list @ X0 > nat > X0))).
% 7.74/1.49 thf(func_def_140, type, sK39: !>[X0: $tType]:((option @ X0 > X0))).
% 7.74/1.49 thf(func_def_141, type, sK40: !>[X0: $tType]:((option @ X0 > X0))).
% 7.74/1.49 thf(func_def_143, type, db3: !>[X0: $tType]:(X0)).
% 7.74/1.49 thf(func_def_144, type, sK42: !>[X0: $tType]:(((option @ X0 > $o) > option @ X0))).
% 7.74/1.49 thf(func_def_145, type, sK43: !>[X0: $tType]:(((option @ X0 > $o) > X0))).
% 7.74/1.49 thf(func_def_146, type, sK44: !>[X0: $tType]:(((option @ X0 > $o) > X0))).
% 7.74/1.49 thf(func_def_147, type, sK45: !>[X0: $tType]:(((option @ X0 > $o) > option @ X0))).
% 7.74/1.49 thf(func_def_148, type, db4: !>[X0: $tType]:(X0)).
% 7.74/1.49 thf(func_def_149, type, db6: !>[X0: $tType]:(X0)).
% 7.74/1.49 thf(func_def_150, type, db5: !>[X0: $tType]:(X0)).
% 7.74/1.49 thf(f18,axiom,(
% 7.74/1.49 ! [X0 : binDag_Mirabelle_dag,X1 : simpl_ref,X2 : binDag_Mirabelle_dag] : (((binDag1924123185ze_dag @ (binDag476092410e_Node @ X0 @ X1 @ X2))) = ((plus_plus @ nat @ (plus_plus @ nat @ (binDag1924123185ze_dag @ X0) @ (binDag1924123185ze_dag @ X2)) @ (suc @ zero_zero @ nat))))),
% 7.74/1.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_17_dag_Osize__gen_I2_J)).
% 7.74/1.49 thf(f38,axiom,(
% 7.74/1.49 ! [X0 : nat,X1 : nat] : (((plus_plus @ nat @ X0 @ (suc @ X1))) = ((suc @ (plus_plus @ nat @ X0 @ X1))))),
% 7.74/1.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_37_add__Suc__right)).
% 7.74/1.49 thf(f73,axiom,(
% 7.74/1.49 ! [X0 : nat] : (zero_zero @ nat != ((suc @ X0)))),
% 7.74/1.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_72_Zero__not__Suc)).
% 7.74/1.49 thf(f77,axiom,(
% 7.74/1.49 ! [X0 : nat] : (((plus_plus @ nat @ zero_zero @ nat @ X0)) = X0)),
% 7.74/1.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_76_plus__nat_Oadd__0)).
% 7.74/1.49 thf(f78,axiom,(
% 7.74/1.49 ! [X0 : nat,X1 : nat] : ((((plus_plus @ nat @ X0 @ X1)) = X0) => (X1 = zero_zero @ nat))),
% 7.74/1.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_77_add__eq__self__zero)).
% 7.74/1.49 thf(f144,axiom,(
% 7.74/1.49 ! [X0 : $tType,X1 : (product_unit > X0)] : ((^[X2 : product_unit] : ((X1 @ product_Unity))) = X1)),
% 7.74/1.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_143_unit__abs__eta__conv)).
% 7.74/1.49 thf(f145,axiom,(
% 7.74/1.49 ! [X0 : $tType,X1 : X0] : (((product_rec_unit @ X0 @ X1 @ product_Unity)) = X1)),
% 7.74/1.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_144_old_Ounit_Orec)).
% 7.74/1.49 thf(f221,axiom,(
% 7.74/1.49 (suc = (^[X0 : nat] : ((plus_plus @ nat @ X0 @ one_one @ nat))))),
% 7.74/1.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_220_Suc__eq__plus1)).
% 7.74/1.49 thf(f370,conjecture,(
% 7.74/1.49 (((binDag476092410e_Node @ lt @ a @ rt)) != lt)),
% 7.74/1.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 7.74/1.49 thf(f371,negated_conjecture,(
% 7.74/1.49 ~ (((binDag476092410e_Node @ lt @ a @ rt)) != lt)),
% 7.74/1.49 inference(negated_conjecture,[status(cth)],[f370])).
% 7.74/1.49 thf(f505,plain,(
% 7.74/1.49 ! [X0 : $tType,X1 : (product_unit > X0)] : ((^[Y0 : product_unit]: (X1 @ product_Unity)) = X1)),
% 7.74/1.49 inference(fool_elimination,[],[f144])).
% 7.74/1.49 thf(f566,plain,(
% 7.74/1.49 (suc = (^[Y0 : nat]: (plus_plus @ nat @ Y0 @ one_one @ nat)))),
% 7.74/1.49 inference(fool_elimination,[],[f221])).
% 7.74/1.49 thf(f851,plain,(
% 7.74/1.49 (lt = ((binDag476092410e_Node @ lt @ a @ rt)))),
% 7.74/1.49 inference(flattening,[],[f371])).
% 7.74/1.49 thf(f896,plain,(
% 7.74/1.49 ! [X0 : nat,X1 : nat] : ((X1 = zero_zero @ nat) | (((plus_plus @ nat @ X0 @ X1)) != X0))),
% 7.74/1.49 inference(ennf_transformation,[],[f78])).
% 7.74/1.49 thf(f1064,plain,(
% 7.74/1.49 ( ! [X2 : binDag_Mirabelle_dag,X0 : binDag_Mirabelle_dag,X1 : simpl_ref] : ((((binDag1924123185ze_dag @ (binDag476092410e_Node @ X0 @ X1 @ X2))) = ((plus_plus @ nat @ (plus_plus @ nat @ (binDag1924123185ze_dag @ X0) @ (binDag1924123185ze_dag @ X2)) @ (suc @ zero_zero @ nat))))) )),
% 7.74/1.49 inference(cnf_transformation,[],[f18])).
% 7.74/1.49 thf(f1084,plain,(
% 7.74/1.49 ( ! [X0 : nat,X1 : nat] : ((((plus_plus @ nat @ X0 @ (suc @ X1))) = ((suc @ (plus_plus @ nat @ X0 @ X1))))) )),
% 7.74/1.49 inference(cnf_transformation,[],[f38])).
% 7.74/1.49 thf(f1122,plain,(
% 7.74/1.49 ( ! [X0 : nat] : ((zero_zero @ nat != ((suc @ X0)))) )),
% 7.74/1.49 inference(cnf_transformation,[],[f73])).
% 7.74/1.49 thf(f1127,plain,(
% 7.74/1.49 ( ! [X0 : nat] : ((((plus_plus @ nat @ zero_zero @ nat @ X0)) = X0)) )),
% 7.74/1.49 inference(cnf_transformation,[],[f77])).
% 7.74/1.49 thf(f1128,plain,(
% 7.74/1.49 ( ! [X0 : nat,X1 : nat] : ((((plus_plus @ nat @ X0 @ X1)) != X0) | (zero_zero @ nat = X1)) )),
% 7.74/1.49 inference(cnf_transformation,[],[f896])).
% 7.74/1.49 thf(f1208,plain,(
% 7.74/1.49 ( ! [X0 : $tType,X1 : (product_unit > X0)] : (((^[Y0 : product_unit]: (X1 @ product_Unity)) = X1)) )),
% 7.74/1.49 inference(cnf_transformation,[],[f505])).
% 7.74/1.49 thf(f1209,plain,(
% 7.74/1.49 ( ! [X0 : $tType,X1 : X0] : ((((product_rec_unit @ X0 @ X1 @ product_Unity)) = X1)) )),
% 7.74/1.49 inference(cnf_transformation,[],[f145])).
% 7.74/1.49 thf(f1294,plain,(
% 7.74/1.49 (suc = (^[Y0 : nat]: (plus_plus @ nat @ Y0 @ one_one @ nat)))),
% 7.74/1.49 inference(cnf_transformation,[],[f566])).
% 7.74/1.49 thf(f1444,plain,(
% 7.74/1.49 (lt = ((binDag476092410e_Node @ lt @ a @ rt)))),
% 7.74/1.49 inference(cnf_transformation,[],[f851])).
% 7.74/1.49 thf(f1451,plain,(
% 7.74/1.49 ( ! [X2 : binDag_Mirabelle_dag,X0 : binDag_Mirabelle_dag,X1 : simpl_ref] : ((((binDag1924123185ze_dag @ (binDag476092410e_Node @ X0 @ X1 @ X2))) = ((plus_plus @ nat @ (plus_plus @ nat @ (binDag1924123185ze_dag @ X0) @ (binDag1924123185ze_dag @ X2)) @ ((^[Y0 : nat]: (plus_plus @ nat @ Y0 @ one_one @ nat)) @ zero_zero @ nat))))) )),
% 7.74/1.49 inference(definition_unfolding,[],[f1064,f1294])).
% 7.74/1.49 thf(f1455,plain,(
% 7.74/1.49 ( ! [X0 : nat,X1 : nat] : ((((plus_plus @ nat @ X0 @ ((^[Y0 : nat]: (plus_plus @ nat @ Y0 @ one_one @ nat)) @ X1))) = (((^[Y0 : nat]: (plus_plus @ nat @ Y0 @ one_one @ nat)) @ (plus_plus @ nat @ X0 @ X1))))) )),
% 7.74/1.49 inference(definition_unfolding,[],[f1084,f1294,f1294])).
% 7.74/1.49 thf(f1472,plain,(
% 7.74/1.49 ( ! [X0 : nat] : ((zero_zero @ nat != (((^[Y0 : nat]: (plus_plus @ nat @ Y0 @ one_one @ nat)) @ X0)))) )),
% 7.74/1.49 inference(definition_unfolding,[],[f1122,f1294])).
% 7.74/1.49 thf(f1917,plain,(
% 7.74/1.49 ( ! [X0 : nat] : ((zero_zero @ nat != ((plus_plus @ nat @ X0 @ one_one @ nat)))) )),
% 7.74/1.49 inference(beta-eta_normalization,[],[f1472])).
% 7.74/1.49 thf(f2033,plain,(
% 7.74/1.49 ( ! [X0 : nat,X1 : nat] : ((((plus_plus @ nat @ (plus_plus @ nat @ X0 @ X1) @ one_one @ nat)) = ((plus_plus @ nat @ X0 @ (plus_plus @ nat @ X1 @ one_one @ nat))))) )),
% 7.74/1.49 inference(beta-eta_normalization,[],[f1455])).
% 7.74/1.49 thf(f2110,plain,(
% 7.74/1.49 ( ! [X2 : binDag_Mirabelle_dag,X0 : binDag_Mirabelle_dag,X1 : simpl_ref] : ((((binDag1924123185ze_dag @ (binDag476092410e_Node @ X0 @ X1 @ X2))) = ((plus_plus @ nat @ (plus_plus @ nat @ (binDag1924123185ze_dag @ X0) @ (binDag1924123185ze_dag @ X2)) @ (plus_plus @ nat @ zero_zero @ nat @ one_one @ nat))))) )),
% 7.74/1.49 inference(beta-eta_normalization,[],[f1451])).
% 7.74/1.49 thf(f2164,plain,(
% 7.74/1.49 ( ! [X0 : $tType,X2 : product_unit,X1 : (product_unit > X0)] : (((((^[Y0 : product_unit]: (X1 @ product_Unity)) @ X2)) = ((X1 @ X2)))) )),
% 7.74/1.49 inference(argument_congruence,[],[f1208])).
% 7.74/1.49 thf(f2166,plain,(
% 7.74/1.49 ( ! [X0 : $tType,X2 : product_unit,X1 : (product_unit > X0)] : ((((X1 @ product_Unity)) = ((X1 @ X2)))) )),
% 7.74/1.49 inference(beta-eta_normalization,[],[f2164])).
% 7.74/1.49 thf(f2180,plain,(
% 7.74/1.49 ( ! [X2 : product_unit,X0 : (product_unit > binDag_Mirabelle_dag),X1 : (product_unit > simpl_ref)] : ((lt = (((^[Y0 : product_unit]: (binDag476092410e_Node @ (X0 @ Y0) @ (X1 @ Y0) @ ((^[Y1 : product_unit]: (rt)) @ Y0))) @ X2))) | (a != ((X1 @ product_Unity))) | (lt != ((X0 @ product_Unity)))) )),
% 7.74/1.49 inference(constrained_superposition,[],[f2166,f1444])).
% 7.74/1.49 thf(f2622,plain,(
% 7.74/1.49 ( ! [X2 : product_unit,X0 : (product_unit > binDag_Mirabelle_dag),X1 : (product_unit > simpl_ref)] : ((lt != ((X0 @ product_Unity))) | (a != ((X1 @ product_Unity))) | (lt = ((binDag476092410e_Node @ (X0 @ X2) @ (X1 @ X2) @ rt)))) )),
% 7.74/1.49 inference(beta-eta_normalization,[],[f2180])).
% 7.74/1.49 thf(f3324,plain,(
% 7.74/1.49 ( ! [X0 : (product_unit > simpl_ref),X1 : product_unit] : ((a != ((X0 @ product_Unity))) | (lt = ((binDag476092410e_Node @ ((^[Y0 : product_unit]: (lt)) @ X1) @ (X0 @ X1) @ rt)))) )),
% 7.74/1.49 inference(equality_resolution,[],[f2622])).
% 7.74/1.49 thf(f3325,plain,(
% 7.74/1.49 ( ! [X0 : (product_unit > simpl_ref),X1 : product_unit] : ((a != ((X0 @ product_Unity))) | (lt = ((binDag476092410e_Node @ lt @ (X0 @ X1) @ rt)))) )),
% 7.74/1.49 inference(beta-eta_normalization,[],[f3324])).
% 7.74/1.49 thf(f3407,plain,(
% 7.74/1.49 ( ! [X2 : product_unit,X0 : simpl_ref,X1 : (product_unit > simpl_ref)] : ((a != X0) | (lt = ((binDag476092410e_Node @ lt @ ((^[Y0 : product_unit]: (product_rec_unit @ simpl_ref @ (X1 @ Y0) @ ((^[Y1 : product_unit]: (Y1)) @ Y0))) @ X2) @ rt))) | (((X1 @ product_Unity)) != X0)) )),
% 7.74/1.49 inference(constrained_superposition,[],[f3325,f1209])).
% 7.74/1.49 thf(f3414,plain,(
% 7.74/1.49 ( ! [X2 : product_unit,X0 : simpl_ref,X1 : (product_unit > simpl_ref)] : ((a != X0) | (lt = ((binDag476092410e_Node @ lt @ (product_rec_unit @ simpl_ref @ (X1 @ X2) @ X2) @ rt))) | (((X1 @ product_Unity)) != X0)) )),
% 7.74/1.49 inference(beta-eta_normalization,[],[f3407])).
% 7.74/1.49 thf(f8838,plain,(
% 7.74/1.49 ( ! [X0 : (product_unit > simpl_ref),X1 : product_unit] : ((a != ((X0 @ product_Unity))) | (lt = ((binDag476092410e_Node @ lt @ (product_rec_unit @ simpl_ref @ (X0 @ X1) @ X1) @ rt)))) )),
% 7.74/1.49 inference(equality_resolution,[],[f3414])).
% 7.74/1.49 thf(f8857,plain,(
% 7.74/1.49 ( ! [X0 : product_unit] : ((lt = ((binDag476092410e_Node @ lt @ (product_rec_unit @ simpl_ref @ ((^[Y0 : product_unit]: (a)) @ X0) @ X0) @ rt)))) )),
% 7.74/1.49 inference(equality_resolution,[],[f8838])).
% 7.74/1.49 thf(f8858,plain,(
% 7.74/1.49 ( ! [X0 : product_unit] : ((lt = ((binDag476092410e_Node @ lt @ (product_rec_unit @ simpl_ref @ a @ X0) @ rt)))) )),
% 7.74/1.49 inference(beta-eta_normalization,[],[f8857])).
% 7.74/1.49 thf(f17666,plain,(
% 7.74/1.49 ( ! [X2 : binDag_Mirabelle_dag,X0 : binDag_Mirabelle_dag,X1 : simpl_ref] : ((((binDag1924123185ze_dag @ (binDag476092410e_Node @ X0 @ X1 @ X2))) = ((plus_plus @ nat @ (plus_plus @ nat @ (binDag1924123185ze_dag @ X0) @ (binDag1924123185ze_dag @ X2)) @ one_one @ nat)))) )),
% 7.74/1.49 inference(forward_demodulation,[],[f2110,f1127])).
% 7.74/1.49 thf(f17667,plain,(
% 7.74/1.49 (((binDag1924123185ze_dag @ lt)) = ((plus_plus @ nat @ (plus_plus @ nat @ (binDag1924123185ze_dag @ lt) @ (binDag1924123185ze_dag @ rt)) @ one_one @ nat)))),
% 7.74/1.49 inference(constrained_superposition,[],[f17666,f8858])).
% 7.74/1.49 thf(f18242,plain,(
% 7.74/1.49 (((binDag1924123185ze_dag @ lt)) = ((plus_plus @ nat @ (binDag1924123185ze_dag @ lt) @ (plus_plus @ nat @ (binDag1924123185ze_dag @ rt) @ one_one @ nat))))),
% 7.74/1.49 inference(constrained_superposition,[],[f17667,f2033])).
% 7.74/1.49 thf(f19651,plain,(
% 7.74/1.49 (((binDag1924123185ze_dag @ lt)) != ((binDag1924123185ze_dag @ lt))) | (zero_zero @ nat = ((plus_plus @ nat @ (binDag1924123185ze_dag @ rt) @ one_one @ nat)))),
% 7.74/1.49 inference(constrained_superposition,[],[f1128,f18242])).
% 7.74/1.49 thf(f19652,plain,(
% 7.74/1.49 (zero_zero @ nat = ((plus_plus @ nat @ (binDag1924123185ze_dag @ rt) @ one_one @ nat)))),
% 7.74/1.49 inference(trivial_inequality_removal,[],[f19651])).
% 7.74/1.49 thf(f19656,plain,(
% 7.74/1.49 $false),
% 7.74/1.49 inference(forward_subsumption_resolution,[],[f19652,f1917])).
% 7.74/1.49 % SZS output end Proof for theBenchmark
% 7.74/1.49 % (2987601)------------------------------
% 7.74/1.49 % (2987601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.49 % (2987601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.49 % (2987601)CaDiCaL version: 2.1.3
% 7.74/1.49 % (2987601)Termination reason: Refutation
% 7.74/1.49 % (2987601)Time elapsed: 1.190 s
% 7.74/1.49 % (2987601)Peak memory usage: 25 MB
% 7.74/1.49 % (2987601)Instructions burned: 2242 (million)
% 7.74/1.49 % (2987595)Success in time 1.249 s
% 7.74/1.49 % Vampire exiting
%------------------------------------------------------------------------------