%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : COM193^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 : n004.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:31 AM UTC 2026
% Result : Theorem 34.28s 5.15s
% Output : Refutation 34.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM193^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n004.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 17:50:52 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/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
% 8.29/1.44 % (1629713)Will run a generic schedule for satisfiability detection.
% 8.29/1.44 % (1629721)dis+10_1_sil=32000:sp=arity:random_seed=2133783142:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.29/1.44 % (1629719)% WARNING: option uhcvi not known.
% 8.29/1.44 % (1629719)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=261332961:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.29/1.44 % (1629718)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3700085864_2999 on theBenchmark for (2999ds/0Mi)
% 8.29/1.44 % (1629720)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=385584174:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.29/1.44 % (1629723)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2665240459:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.29/1.44 % (1629722)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2806243402:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.29/1.44 % (1629724)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3604552307:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.29/1.44 % (1629719)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 8.29/1.44 % (1629722)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 8.29/1.44 % (1629721)Instruction limit reached!
% 8.29/1.44 % (1629721)------------------------------
% 8.29/1.44 % (1629721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.29/1.44 % (1629721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.29/1.44 % (1629721)CaDiCaL version: 2.1.3
% 8.29/1.44 % (1629721)Termination reason: Instruction limit
% 8.29/1.44 % (1629721)Termination phase: Saturation
% 8.29/1.44 % (1629721)Time elapsed: 0.032 s
% 8.29/1.44 % (1629721)Peak memory usage: 13 MB
% 8.29/1.44 % (1629721)Instructions burned: 105 (million)
% 8.29/1.44 % (1629719)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 8.29/1.44 % Exception at run slice level
% 8.29/1.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.29/1.44 % (1629732)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=415639029:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.29/1.44 % Exception at run slice level
% 8.29/1.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.29/1.44 % (1629734)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3723926532:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 8.29/1.44 % (1629722)Instruction limit reached!
% 8.29/1.44 % (1629722)------------------------------
% 8.29/1.44 % (1629722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.29/1.44 % (1629722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.29/1.44 % (1629722)CaDiCaL version: 2.1.3
% 8.29/1.44 % (1629722)Termination reason: Instruction limit
% 8.29/1.44 % (1629722)Termination phase: Saturation
% 8.29/1.44 % (1629722)Time elapsed: 0.054 s
% 8.29/1.44 % (1629722)Peak memory usage: 13 MB
% 8.29/1.44 % (1629722)Instructions burned: 117 (million)
% 8.29/1.44 % (1629735)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=2122640487:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.29/1.44 % (1629735)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 8.29/1.44 % (1629737)ott-21_1_sil=16000:fs=off:random_seed=1185835285:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.29/1.44 % (1629735)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 8.29/1.44 % (1629724)Instruction limit reached!
% 8.29/1.44 % (1629724)------------------------------
% 8.29/1.44 % (1629724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.29/1.44 % (1629724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.29/1.44 % (1629724)CaDiCaL version: 2.1.3
% 8.29/1.44 % (1629724)Termination reason: Instruction limit
% 8.29/1.44 % (1629724)Termination phase: Saturation
% 8.29/1.44 % (1629724)Time elapsed: 0.079 s
% 8.29/1.44 % (1629724)Peak memory usage: 14 MB
% 8.29/1.44 % (1629724)Instructions burned: 160 (million)
% 8.29/1.44 % (1629740)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=335720667:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 21.76/3.37 % (1629734)Instruction limit reached!
% 21.76/3.37 % (1629734)------------------------------
% 21.76/3.37 % (1629734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.76/3.37 % (1629734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.76/3.37 % (1629734)CaDiCaL version: 2.1.3
% 21.76/3.37 % (1629734)Termination reason: Instruction limit
% 21.76/3.37 % (1629734)Termination phase: Saturation
% 21.76/3.37 % (1629734)Time elapsed: 0.061 s
% 21.76/3.37 % (1629734)Peak memory usage: 13 MB
% 21.76/3.37 % (1629734)Instructions burned: 131 (million)
% 21.76/3.37 % (1629723)Instruction limit reached!
% 21.76/3.37 % (1629723)------------------------------
% 21.76/3.37 % (1629723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.76/3.37 % (1629723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.76/3.37 % (1629723)CaDiCaL version: 2.1.3
% 21.76/3.37 % (1629723)Termination reason: Instruction limit
% 21.76/3.37 % (1629723)Termination phase: Saturation
% 21.76/3.37 % (1629723)Time elapsed: 0.114 s
% 21.76/3.37 % (1629723)Peak memory usage: 13 MB
% 21.76/3.37 % (1629723)Instructions burned: 133 (million)
% 21.76/3.37 % (1629742)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3749172068:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 21.76/3.37 % (1629743)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2897686936:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 21.76/3.37 % (1629737)Instruction limit reached!
% 21.76/3.37 % (1629737)------------------------------
% 21.76/3.37 % (1629737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.76/3.37 % (1629737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.76/3.37 % (1629737)CaDiCaL version: 2.1.3
% 21.76/3.37 % (1629737)Termination reason: Instruction limit
% 21.76/3.37 % (1629737)Termination phase: Saturation
% 21.76/3.37 % (1629737)Time elapsed: 0.080 s
% 21.76/3.37 % (1629737)Peak memory usage: 13 MB
% 21.76/3.37 % (1629737)Instructions burned: 181 (million)
% 21.76/3.37 % Exception at run slice level
% 21.76/3.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.76/3.37 % (1629746)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2161896796:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 21.76/3.37 % (1629747)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=146184078: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)
% 21.76/3.37 % (1629747)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 21.76/3.37 % Exception at run slice level
% 21.76/3.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.76/3.37 % (1629750)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2701970087:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 21.76/3.37 % (1629735)Instruction limit reached!
% 21.76/3.37 % (1629735)------------------------------
% 21.76/3.37 % (1629735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.76/3.37 % (1629735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.76/3.37 % (1629735)CaDiCaL version: 2.1.3
% 21.76/3.37 % (1629735)Termination reason: Instruction limit
% 21.76/3.37 % (1629735)Termination phase: Saturation
% 21.76/3.37 % (1629735)Time elapsed: 0.178 s
% 21.76/3.37 % (1629735)Peak memory usage: 19 MB
% 21.76/3.37 % (1629735)Instructions burned: 684 (million)
% 21.76/3.37 % (1629750)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 21.76/3.37 % (1629752)fmb+10_1_sil=64000:random_seed=1224018250:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 21.76/3.37 % (1629752)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 21.76/3.37 % Exception at run slice level
% 21.76/3.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.76/3.37 % (1629754)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=578037213:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 21.76/3.37 % Exception at run slice level
% 21.76/3.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.28/5.15 % (1629756)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1382370504:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 34.28/5.15 % Exception at run slice level
% 34.28/5.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.28/5.15 % (1629758)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1853383166:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 34.28/5.15 % (1629758)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 34.28/5.15 % (1629740)Instruction limit reached!
% 34.28/5.15 % (1629740)------------------------------
% 34.28/5.15 % (1629740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629740)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629740)Termination reason: Instruction limit
% 34.28/5.15 % (1629740)Termination phase: Saturation
% 34.28/5.15 % (1629740)Time elapsed: 0.268 s
% 34.28/5.15 % (1629740)Peak memory usage: 15 MB
% 34.28/5.15 % (1629740)Instructions burned: 477 (million)
% 34.28/5.15 % (1629761)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2629601312:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 34.28/5.15 % (1629761)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 34.28/5.15 % (1629761)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 34.28/5.15 % (1629747)Instruction limit reached!
% 34.28/5.15 % (1629747)------------------------------
% 34.28/5.15 % (1629747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629747)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629747)Termination reason: Instruction limit
% 34.28/5.15 % (1629747)Termination phase: Saturation
% 34.28/5.15 % (1629747)Time elapsed: 0.364 s
% 34.28/5.15 % (1629747)Peak memory usage: 16 MB
% 34.28/5.15 % (1629747)Instructions burned: 693 (million)
% 34.28/5.15 % (1629765)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3284454493:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 34.28/5.15 % Exception at run slice level
% 34.28/5.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.28/5.15 % (1629767)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3829867536:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 34.28/5.15 % Exception at run slice level
% 34.28/5.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.28/5.15 % (1629769)ott-2_1_sil=16000:newcnf=on:random_seed=1586174373:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi)
% 34.28/5.15 % (1629769)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 34.28/5.15 % (1629750)Instruction limit reached!
% 34.28/5.15 % (1629750)------------------------------
% 34.28/5.15 % (1629750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629750)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629750)Termination reason: Instruction limit
% 34.28/5.15 % (1629750)Termination phase: Saturation
% 34.28/5.15 % (1629750)Time elapsed: 0.460 s
% 34.28/5.15 % (1629750)Peak memory usage: 19 MB
% 34.28/5.15 % (1629750)Instructions burned: 880 (million)
% 34.28/5.15 % (1629771)ott+10_1_sil=32000:tgt=ground:random_seed=639564890:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 34.28/5.15 % (1629769)Instruction limit reached!
% 34.28/5.15 % (1629769)------------------------------
% 34.28/5.15 % (1629769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629769)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629769)Termination reason: Instruction limit
% 34.28/5.15 % (1629769)Termination phase: Saturation
% 34.28/5.15 % (1629769)Time elapsed: 0.444 s
% 34.28/5.15 % (1629769)Peak memory usage: 19 MB
% 34.28/5.15 % (1629769)Instructions burned: 871 (million)
% 34.28/5.15 % (1629785)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3085364486:i=54282_2988 on theBenchmark for (2988ds/54282Mi)
% 34.28/5.15 % Exception at run slice level
% 34.28/5.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.28/5.15 % (1629743)Instruction limit reached!
% 34.28/5.15 % (1629743)------------------------------
% 34.28/5.15 % (1629743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629743)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629743)Termination reason: Instruction limit
% 34.28/5.15 % (1629743)Termination phase: Saturation
% 34.28/5.15 % (1629743)Time elapsed: 1.043 s
% 34.28/5.15 % (1629743)Peak memory usage: 19 MB
% 34.28/5.15 % (1629743)Instructions burned: 1179 (million)
% 34.28/5.15 % (1629787)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=749509692:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi)
% 34.28/5.15 % (1629788)dis+21_1_sil=32000:sas=cadical:random_seed=1803327227:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi)
% 34.28/5.15 % (1629787)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 34.28/5.15 % (1629761)Instruction limit reached!
% 34.28/5.15 % (1629761)------------------------------
% 34.28/5.15 % (1629761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629761)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629761)Termination reason: Instruction limit
% 34.28/5.15 % (1629761)Termination phase: Saturation
% 34.28/5.15 % (1629761)Time elapsed: 0.917 s
% 34.28/5.15 % (1629761)Peak memory usage: 16 MB
% 34.28/5.15 % (1629761)Instructions burned: 1474 (million)
% 34.28/5.15 % (1629791)ott+11_1_sil=16000:gs=on:random_seed=1808364168:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi)
% 34.28/5.15 % (1629791)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 34.28/5.15 % (1629758)Instruction limit reached!
% 34.28/5.15 % (1629758)------------------------------
% 34.28/5.15 % (1629758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629758)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629758)Termination reason: Instruction limit
% 34.28/5.15 % (1629758)Termination phase: Saturation
% 34.28/5.15 % (1629758)Time elapsed: 1.372 s
% 34.28/5.15 % (1629758)Peak memory usage: 26 MB
% 34.28/5.15 % (1629758)Instructions burned: 5135 (million)
% 34.28/5.15 % (1629793)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1300973408:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi)
% 34.28/5.15 % Exception at run slice level
% 34.28/5.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.28/5.15 % (1629795)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=278485954:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi)
% 34.28/5.15 % (1629791)Instruction limit reached!
% 34.28/5.15 % (1629791)------------------------------
% 34.28/5.15 % (1629791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629791)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629791)Termination reason: Instruction limit
% 34.28/5.15 % (1629791)Termination phase: Saturation
% 34.28/5.15 % (1629791)Time elapsed: 1.015 s
% 34.28/5.15 % (1629791)Peak memory usage: 20 MB
% 34.28/5.15 % (1629791)Instructions burned: 2254 (million)
% 34.28/5.15 % (1629797)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2697818368:i=29340_2975 on theBenchmark for (2975ds/29340Mi)
% 34.28/5.15 % (1629795)Instruction limit reached!
% 34.28/5.15 % (1629795)------------------------------
% 34.28/5.15 % (1629795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629795)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629795)Termination reason: Instruction limit
% 34.28/5.15 % (1629795)Termination phase: Saturation
% 34.28/5.15 % (1629795)Time elapsed: 1.336 s
% 34.28/5.15 % (1629795)Peak memory usage: 30 MB
% 34.28/5.15 % (1629795)Instructions burned: 4592 (million)
% 34.28/5.15 % (1629799)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1780147857:i=5211_2968 on theBenchmark for (2968ds/5211Mi)
% 34.28/5.15 % (1629788)Instruction limit reached!
% 34.28/5.15 % (1629788)------------------------------
% 34.28/5.15 % (1629788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629788)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629788)Termination reason: Instruction limit
% 34.28/5.15 % (1629788)Termination phase: Saturation
% 34.28/5.15 % (1629788)Time elapsed: 1.892 s
% 34.28/5.15 % (1629788)Peak memory usage: 28 MB
% 34.28/5.15 % (1629788)Instructions burned: 3773 (million)
% 34.28/5.15 % (1629801)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3348965062:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi)
% 34.28/5.15 % (1629787)Instruction limit reached!
% 34.28/5.15 % (1629787)------------------------------
% 34.28/5.15 % (1629787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629787)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629787)Termination reason: Instruction limit
% 34.28/5.15 % (1629787)Termination phase: Saturation
% 34.28/5.15 % (1629787)Time elapsed: 1.961 s
% 34.28/5.15 % (1629787)Peak memory usage: 29 MB
% 34.28/5.15 % (1629787)Instructions burned: 3514 (million)
% 34.28/5.15 % Exception at run slice level
% 34.28/5.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.28/5.15 % (1629803)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1230382202:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi)
% 34.28/5.15 % (1629804)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3111542191:i=14071_2967 on theBenchmark for (2967ds/14071Mi)
% 34.28/5.15 % Exception at run slice level
% 34.28/5.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.28/5.15 % Exception at run slice level
% 34.28/5.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.28/5.15 % (1629807)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1150689433:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi)
% 34.28/5.15 % (1629808)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=991427768:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi)
% 34.28/5.15 % (1629771)Instruction limit reached!
% 34.28/5.15 % (1629771)------------------------------
% 34.28/5.15 % (1629771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629771)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629771)Termination reason: Instruction limit
% 34.28/5.15 % (1629771)Termination phase: Saturation
% 34.28/5.15 % (1629771)Time elapsed: 2.562 s
% 34.28/5.15 % (1629771)Peak memory usage: 38 MB
% 34.28/5.15 % (1629771)Instructions burned: 5116 (million)
% 34.28/5.15 % (1629811)dis+10_16:1_sil=16000:random_seed=4291392776:i=9155:fsr=off_2966 on theBenchmark for (2966ds/9155Mi)
% 34.28/5.15 % (1629799)Instruction limit reached!
% 34.28/5.15 % (1629799)------------------------------
% 34.28/5.15 % (1629799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.15 % (1629799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.15 % (1629799)CaDiCaL version: 2.1.3
% 34.28/5.15 % (1629799)Termination reason: Instruction limit
% 34.28/5.15 % (1629799)Termination phase: Saturation
% 34.28/5.15 % (1629799)Time elapsed: 1.425 s
% 34.28/5.15 % (1629799)Peak memory usage: 40 MB
% 34.28/5.15 % (1629799)Instructions burned: 5216 (million)
% 34.28/5.15 % (1629813)ott-3_8_sil=64000:random_seed=2192085678:i=20139:bs=on_2954 on theBenchmark for (2954ds/20139Mi)
% 34.28/5.15 % (1629808) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1629713-1629808"...
% 34.28/5.15 % (1629808)...printing done.
% 34.28/5.15 % (1629808)Refutation found. Thanks to Tanya!
% 34.28/5.15 % SZS status Theorem for theBenchmark
% 34.28/5.15 % SZS output start Proof for theBenchmark
% 34.28/5.15 thf(type_def_5, type, sum_sum: ($tType * $tType) > $tType).
% 34.28/5.15 thf(type_def_6, type, dtree: $tType).
% 34.28/5.15 thf(type_def_7, type, set: $tType > $tType).
% 34.28/5.15 thf(type_def_8, type, t: $tType).
% 34.28/5.15 thf(type_def_9, type, n: $tType).
% 34.28/5.15 thf(type_def_10, type, itself: $tType > $tType).
% 34.28/5.15 thf(type_def_11, type, sTfun: ($tType * $tType) > $tType).
% 34.28/5.15 thf(func_def_0, type, type: !>[X0: $tType]:((itself @ X0 > $o))).
% 34.28/5.15 thf(func_def_1, type, bot: !>[X0: $tType]:((itself @ X0 > $o))).
% 34.28/5.15 thf(func_def_2, type, ord: !>[X0: $tType]:((itself @ X0 > $o))).
% 34.28/5.15 thf(func_def_3, type, top: !>[X0: $tType]:((itself @ X0 > $o))).
% 34.28/5.15 thf(func_def_4, type, order: !>[X0: $tType]:((itself @ X0 > $o))).
% 34.28/5.15 thf(func_def_5, type, linorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 34.28/5.15 thf(func_def_6, type, preorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 34.28/5.15 thf(func_def_7, type, order_bot: !>[X0: $tType]:((itself @ X0 > $o))).
% 34.28/5.15 thf(func_def_8, type, order_top: !>[X0: $tType]:((itself @ X0 > $o))).
% 34.28/5.15 thf(func_def_9, type, boolean_algebra: !>[X0: $tType]:((itself @ X0 > $o))).
% 34.28/5.15 thf(func_def_10, type, ordered_ab_group_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 34.28/5.15 thf(func_def_11, type, node: (n > set @ sum_sum @ t @ dtree > dtree)).
% 34.28/5.15 thf(func_def_12, type, corec: !>[X0: $tType]:(((X0 > n) > (X0 > set @ sum_sum @ t @ sum_sum @ dtree @ X0) > X0 > dtree))).
% 34.28/5.15 thf(func_def_13, type, root: (dtree > n)).
% 34.28/5.15 thf(func_def_14, type, unfold: !>[X0: $tType]:(((X0 > n) > (X0 > set @ sum_sum @ t @ X0) > X0 > dtree))).
% 34.28/5.15 thf(func_def_15, type, gram_L861583724lle_Fr: (set @ n > dtree > set @ t)).
% 34.28/5.15 thf(func_def_16, type, gram_L1451583624elle_H: (dtree > n > dtree)).
% 34.28/5.15 thf(func_def_17, type, gram_L1221482011le_H_c: (dtree > n > set @ sum_sum @ t @ n)).
% 34.28/5.15 thf(func_def_18, type, gram_L1221482026le_H_r: (dtree > n > n)).
% 34.28/5.15 thf(func_def_19, type, gram_L1451583628elle_L: (set @ n > n > set @ set @ t)).
% 34.28/5.15 thf(func_def_20, type, gram_L1231612515_deftr: (n > dtree)).
% 34.28/5.15 thf(func_def_21, type, gram_L1004374585hsubst: (dtree > dtree > dtree)).
% 34.28/5.15 thf(func_def_22, type, gram_L1905609002ubst_c: (dtree > dtree > set @ sum_sum @ t @ dtree)).
% 34.28/5.15 thf(func_def_23, type, gram_L1905609017ubst_r: (dtree > n)).
% 34.28/5.15 thf(func_def_24, type, gram_L1333338417e_inFr: (set @ n > dtree > t > $o)).
% 34.28/5.15 thf(func_def_25, type, gram_L830233218_inItr: (set @ n > dtree > n > $o)).
% 34.28/5.15 thf(func_def_26, type, gram_L315592705e_pick: (dtree > n > dtree)).
% 34.28/5.15 thf(func_def_27, type, gram_L1828378864e_rcut: (dtree > dtree)).
% 34.28/5.15 thf(func_def_28, type, gram_L1918716148le_reg: ((n > dtree) > dtree > $o)).
% 34.28/5.15 thf(func_def_29, type, gram_L646766332egular: (dtree > $o)).
% 34.28/5.15 thf(func_def_30, type, gram_L716654942_subtr: (set @ n > dtree > dtree > $o)).
% 34.28/5.15 thf(func_def_31, type, gram_L864798063lle_wf: (dtree > $o)).
% 34.28/5.15 thf(func_def_32, type, minus_minus: !>[X0: $tType]:((X0 > X0 > X0))).
% 34.28/5.15 thf(func_def_33, type, uminus_uminus: !>[X0: $tType]:((X0 > X0))).
% 34.28/5.15 thf(func_def_34, type, bot_bot: !>[X0: $tType]:(X0)).
% 34.28/5.15 thf(func_def_35, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 34.28/5.15 thf(func_def_36, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 34.28/5.15 thf(func_def_37, type, top_top: !>[X0: $tType]:(X0)).
% 34.28/5.15 thf(func_def_38, type, type2: !>[X0: $tType]:(itself @ X0)).
% 34.28/5.15 thf(func_def_39, type, inv_imagep: !>[X0: $tType, X1: $tType]:(((X0 > X0 > $o) > (X1 > X0) > X1 > X1 > $o))).
% 34.28/5.15 thf(func_def_40, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 34.28/5.15 thf(func_def_41, type, pow: !>[X0: $tType]:((set @ X0 > set @ set @ X0))).
% 34.28/5.15 thf(func_def_42, type, insert: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 34.28/5.15 thf(func_def_43, type, is_empty: !>[X0: $tType]:((set @ X0 > $o))).
% 34.28/5.15 thf(func_def_44, type, is_singleton: !>[X0: $tType]:((set @ X0 > $o))).
% 34.28/5.15 thf(func_def_45, type, pairwise: !>[X0: $tType]:(((X0 > X0 > $o) > set @ X0 > $o))).
% 34.28/5.15 thf(func_def_46, type, remove: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 34.28/5.15 thf(func_def_47, type, the_elem: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.15 thf(func_def_48, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 34.28/5.15 thf(func_def_49, type, n2: n).
% 34.28/5.15 thf(func_def_50, type, ns: set @ n).
% 34.28/5.15 thf(func_def_54, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 34.28/5.15 thf(func_def_55, type, vNOT: ($o > $o)).
% 34.28/5.15 thf(func_def_56, type, db0: !>[X0: $tType]:(X0)).
% 34.28/5.15 thf(func_def_57, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 34.28/5.15 thf(func_def_58, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 34.28/5.15 thf(func_def_59, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 34.28/5.15 thf(func_def_60, type, vAND: ($o > $o > $o)).
% 34.28/5.15 thf(func_def_61, type, db1: !>[X0: $tType]:(X0)).
% 34.28/5.15 thf(func_def_62, type, vIMP: ($o > $o > $o)).
% 34.28/5.15 thf(func_def_63, type, db2: !>[X0: $tType]:(X0)).
% 34.28/5.15 thf(func_def_64, type, db3: !>[X0: $tType]:(X0)).
% 34.28/5.15 thf(func_def_65, type, vOR: ($o > $o > $o)).
% 34.28/5.15 thf(func_def_66, type, sP0: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 34.28/5.15 thf(func_def_67, type, sP1: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 34.28/5.15 thf(func_def_68, type, sP2: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 34.28/5.15 thf(func_def_69, type, sK3: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.15 thf(func_def_70, type, sK4: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.15 thf(func_def_71, type, sK5: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.15 thf(func_def_72, type, sK6: (n > dtree > set @ n > dtree)).
% 34.28/5.15 thf(func_def_73, type, sK7: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 34.28/5.15 thf(func_def_74, type, sK8: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 34.28/5.15 thf(func_def_75, type, sK9: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.15 thf(func_def_76, type, sK10: !>[X0: $tType]:((set @ X0 > X0 > set @ X0))).
% 34.28/5.15 thf(func_def_77, type, sK11: !>[X0: $tType]:(X0)).
% 34.28/5.15 thf(func_def_78, type, sK12: !>[X0: $tType]:((set @ X0 > X0 > set @ X0))).
% 34.28/5.15 thf(func_def_79, type, sK13: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.16 thf(func_def_80, type, sK14: (dtree > dtree > n)).
% 34.28/5.16 thf(func_def_81, type, sK15: !>[X0: $tType]:((set @ X0 > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_82, type, sK16: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 34.28/5.16 thf(func_def_83, type, sK17: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 34.28/5.16 thf(func_def_84, type, sK18: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 34.28/5.16 thf(func_def_85, type, sK19: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 34.28/5.16 thf(func_def_86, type, sK20: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 34.28/5.16 thf(func_def_87, type, sK21: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 34.28/5.16 thf(func_def_88, type, sK22: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 34.28/5.16 thf(func_def_89, type, sK23: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 34.28/5.16 thf(func_def_90, type, sK24: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 34.28/5.16 thf(func_def_91, type, sK25: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 34.28/5.16 thf(func_def_92, type, sK26: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 34.28/5.16 thf(func_def_93, type, sK27: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 34.28/5.16 thf(func_def_94, type, sK28: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 34.28/5.16 thf(func_def_95, type, sK29: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 34.28/5.16 thf(func_def_96, type, sK30: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.16 thf(func_def_97, type, sK31: !>[X0: $tType]:((set @ X0 > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_98, type, sK32: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 34.28/5.16 thf(func_def_99, type, sK33: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 34.28/5.16 thf(func_def_100, type, sK34: ((n > dtree) > n)).
% 34.28/5.16 thf(func_def_101, type, sK35: ((n > dtree) > dtree > dtree)).
% 34.28/5.16 thf(func_def_102, type, sK36: ((n > dtree) > dtree > set @ n)).
% 34.28/5.16 thf(func_def_103, type, sK37: !>[X0: $tType]:(((X0 > X0 > $o) > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_104, type, sK38: !>[X0: $tType]:(((X0 > X0 > $o) > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_105, type, sK39: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 34.28/5.16 thf(func_def_106, type, sK40: !>[X0: $tType]:((X0 > set @ X0 > X0 > set @ X0 > set @ X0))).
% 34.28/5.16 thf(func_def_107, type, sK41: !>[X0: $tType]:(((X0 > X0 > $o) > X0 > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_108, type, sK42: !>[X0: $tType]:(((X0 > X0 > $o) > X0 > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_109, type, sK43: !>[X0: $tType]:(((X0 > X0 > $o) > X0 > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_110, type, sK44: !>[X0: $tType]:(((X0 > X0 > $o) > X0 > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_111, type, sK45: !>[X0: $tType]:(((X0 > X0 > $o) > X0 > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_112, type, sK46: !>[X0: $tType]:(((X0 > X0 > $o) > X0 > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_113, type, sK47: !>[X0: $tType]:(((X0 > X0 > $o) > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_114, type, sK48: !>[X0: $tType]:(((X0 > X0 > $o) > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_115, type, sK49: !>[X0: $tType]:(((X0 > X0 > $o) > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_116, type, sK50: !>[X0: $tType]:(((X0 > X0 > $o) > set @ X0 > X0))).
% 34.28/5.16 thf(func_def_117, type, sK51: !>[X0: $tType]:((X0 > X0))).
% 34.28/5.16 thf(func_def_118, type, sK52: (dtree > n > dtree)).
% 34.28/5.16 thf(func_def_119, type, sK53: ((n > dtree) > n)).
% 34.28/5.16 thf(func_def_120, type, sK54: ((n > dtree) > dtree > dtree)).
% 34.28/5.16 thf(func_def_121, type, sK55: ((n > dtree) > dtree > set @ n)).
% 34.28/5.16 thf(func_def_122, type, sK56: ((n > dtree) > n)).
% 34.28/5.16 thf(func_def_123, type, sK57: ((n > dtree) > dtree > dtree)).
% 34.28/5.16 thf(func_def_124, type, sK58: ((n > dtree) > dtree > set @ n)).
% 34.28/5.16 thf(func_def_125, type, sK59: (dtree > (n > dtree) > dtree)).
% 34.28/5.16 thf(func_def_126, type, sK60: (dtree > (n > dtree) > set @ n)).
% 34.28/5.16 thf(func_def_127, type, sK61: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.16 thf(func_def_128, type, sK62: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.16 thf(func_def_129, type, sK63: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.16 thf(func_def_130, type, sK64: (dtree > dtree)).
% 34.28/5.16 thf(func_def_131, type, sK65: (dtree > set @ n)).
% 34.28/5.16 thf(func_def_132, type, sK66: (dtree > dtree)).
% 34.28/5.16 thf(func_def_133, type, sK67: (dtree > set @ n)).
% 34.28/5.16 thf(func_def_134, type, sK68: (dtree > n > dtree)).
% 34.28/5.16 thf(func_def_135, type, sK69: (dtree > (n > dtree) > dtree)).
% 34.28/5.16 thf(func_def_136, type, sK70: (dtree > (n > dtree) > set @ n)).
% 34.28/5.16 thf(func_def_137, type, sK71: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.16 thf(func_def_138, type, sK72: !>[X0: $tType]:(((X0 > $o) > X0))).
% 34.28/5.16 thf(func_def_139, type, sK73: !>[X0: $tType]:(((X0 > $o) > X0))).
% 34.28/5.16 thf(func_def_140, type, sK74: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.16 thf(func_def_141, type, sK75: !>[X0: $tType]:(((X0 > $o) > X0))).
% 34.28/5.16 thf(func_def_142, type, sK76: !>[X0: $tType]:((set @ X0 > X0))).
% 34.28/5.16 thf(func_def_143, type, sK77: (dtree > n > dtree)).
% 34.28/5.16 thf(func_def_144, type, sK78: ((n > dtree) > n)).
% 34.28/5.16 thf(func_def_145, type, sK79: (dtree > (n > dtree) > dtree)).
% 34.28/5.16 thf(func_def_146, type, sK80: (dtree > (n > dtree) > set @ n)).
% 34.28/5.16 thf(func_def_147, type, sK81: (dtree > n > dtree)).
% 34.28/5.16 thf(func_def_148, type, sK82: (dtree > (n > dtree) > dtree)).
% 34.28/5.16 thf(func_def_149, type, sK83: (dtree > (n > dtree) > set @ n)).
% 34.28/5.16 thf(func_def_150, type, sK84: (dtree > (n > dtree) > dtree)).
% 34.28/5.16 thf(func_def_151, type, sK85: (dtree > (n > dtree) > set @ n)).
% 34.28/5.16 thf(f1,axiom,(
% 34.28/5.16 ~(member @ n @ n2 @ ns)),
% 34.28/5.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_assms)).
% 34.28/5.16 thf(f2,axiom,(
% 34.28/5.16 ! [X0 : dtree,X1 : set @ n] : (~(member @ n @ (root @ X0) @ X1) => (((gram_L861583724lle_Fr @ X1 @ X0)) = bot_bot @ set @ t))),
% 34.28/5.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_not__root__Fr)).
% 34.28/5.16 thf(f8,axiom,(
% 34.28/5.16 (gram_L1905609017ubst_r = root)),
% 34.28/5.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_hsubst__r__def)).
% 34.28/5.16 thf(f10,axiom,(
% 34.28/5.16 (gram_L646766332egular = (^[X0 : dtree] : (? [X1 : (n > dtree)] : (! [X2 : n] : (((root @ (X1 @ X2))) = X2) & (gram_L1918716148le_reg @ X1 @ X0)))))),
% 34.28/5.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9_regular__def2)).
% 34.28/5.16 thf(f28,axiom,(
% 34.28/5.16 ! [X0 : n] : (((root @ (gram_L1231612515_deftr @ X0))) = X0)),
% 34.28/5.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_27_root__deftr)).
% 34.28/5.16 thf(f31,axiom,(
% 34.28/5.16 (gram_L1918716148le_reg = (^[X0 : (n > dtree), X1 : dtree] : (! [X2 : set @ n,X3 : dtree] : ((gram_L716654942_subtr @ X2 @ X3 @ X1) => (X3 = ((X0 @ (root @ X3))))))))),
% 34.28/5.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_30_reg__def2)).
% 34.28/5.16 thf(f33,axiom,(
% 34.28/5.16 ! [X0 : set @ n,X1 : dtree,X2 : n] : ((gram_L716654942_subtr @ X0 @ X1 @ (gram_L1231612515_deftr @ X2)) => (X1 = ((gram_L1231612515_deftr @ (root @ X1)))))),
% 34.28/5.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_32_subtr__deftr)).
% 34.28/5.16 thf(f40,axiom,(
% 34.28/5.16 ! [X0 : n] : (gram_L864798063lle_wf @ (gram_L1231612515_deftr @ X0))),
% 34.28/5.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_39_wf__deftr)).
% 34.28/5.16 thf(f283,conjecture,(
% 34.28/5.16 ? [X0 : dtree] : ((gram_L646766332egular @ X0) & (((root @ X0)) = n2) & (gram_L864798063lle_wf @ X0) & (bot_bot @ set @ t = ((gram_L861583724lle_Fr @ ns @ X0))))),
% 34.28/5.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1)).
% 34.28/5.16 thf(f284,negated_conjecture,(
% 34.28/5.16 ~ ? [X0 : dtree] : ((gram_L646766332egular @ X0) & (((root @ X0)) = n2) & (gram_L864798063lle_wf @ X0) & (bot_bot @ set @ t = ((gram_L861583724lle_Fr @ ns @ X0))))),
% 34.28/5.16 inference(negated_conjecture,[status(cth)],[f283])).
% 34.28/5.16 thf(f285,plain,(
% 34.28/5.16 ~(member @ n @ n2 @ ns)),
% 34.28/5.16 inference(rectify,[],[f1])).
% 34.28/5.16 thf(f286,plain,(
% 34.28/5.16 ~ (((member @ n @ n2 @ ns)) = $true)),
% 34.28/5.16 inference(fool_elimination,[],[f285])).
% 34.28/5.16 thf(f287,plain,(
% 34.28/5.16 ! [X0 : dtree,X1 : set @ n] : (~(member @ n @ (root @ X0) @ X1) => (((gram_L861583724lle_Fr @ X1 @ X0)) = bot_bot @ set @ t))),
% 34.28/5.16 inference(rectify,[],[f2])).
% 34.28/5.16 thf(f288,plain,(
% 34.28/5.16 ! [X0 : dtree,X1 : set @ n] : (~ (((member @ n @ (root @ X0) @ X1)) = $true) => (((gram_L861583724lle_Fr @ X1 @ X0)) = bot_bot @ set @ t))),
% 34.28/5.16 inference(fool_elimination,[],[f287])).
% 34.28/5.16 thf(f299,plain,(
% 34.28/5.16 (gram_L646766332egular = (^[X0 : dtree] : (? [X1 : (n > dtree)] : (! [X2 : n] : (((root @ (X1 @ X2))) = X2) & (gram_L1918716148le_reg @ X1 @ X0)))))),
% 34.28/5.16 inference(rectify,[],[f10])).
% 34.28/5.16 thf(f300,plain,(
% 34.28/5.16 (gram_L646766332egular = (^[Y0 : dtree]: (?? @ (n > dtree) @ (^[Y1 : n > dtree]: ((gram_L1918716148le_reg @ Y1 @ Y0) & (!! @ n @ (^[Y2 : n]: ((root @ (Y1 @ Y2)) = Y2))))))))),
% 34.28/5.16 inference(fool_elimination,[],[f299])).
% 34.28/5.16 thf(f332,plain,(
% 34.28/5.16 (gram_L1918716148le_reg = (^[X0 : (n > dtree), X1 : dtree] : (! [X2 : set @ n,X3 : dtree] : ((gram_L716654942_subtr @ X2 @ X3 @ X1) => (X3 = ((X0 @ (root @ X3))))))))),
% 34.28/5.16 inference(rectify,[],[f31])).
% 34.28/5.16 thf(f333,plain,(
% 34.28/5.16 (gram_L1918716148le_reg = (^[Y0 : n > dtree]: ((^[Y1 : dtree]: (!! @ dtree @ (^[Y2 : dtree]: (!! @ set @ n @ (^[Y3 : set @ n]: ((gram_L716654942_subtr @ Y3 @ Y2 @ Y1) => ((Y0 @ (root @ Y2)) = Y2))))))))))),
% 34.28/5.16 inference(fool_elimination,[],[f332])).
% 34.28/5.16 thf(f336,plain,(
% 34.28/5.16 ! [X0 : set @ n,X1 : dtree,X2 : n] : ((gram_L716654942_subtr @ X0 @ X1 @ (gram_L1231612515_deftr @ X2)) => (X1 = ((gram_L1231612515_deftr @ (root @ X1)))))),
% 34.28/5.16 inference(rectify,[],[f33])).
% 34.28/5.16 thf(f337,plain,(
% 34.28/5.16 ! [X0 : set @ n,X1 : dtree,X2 : n] : ((((gram_L716654942_subtr @ X0 @ X1 @ (gram_L1231612515_deftr @ X2))) = $true) => (((gram_L1231612515_deftr @ (root @ X1))) = X1))),
% 34.28/5.16 inference(fool_elimination,[],[f336])).
% 34.28/5.16 thf(f350,plain,(
% 34.28/5.16 ! [X0 : n] : (gram_L864798063lle_wf @ (gram_L1231612515_deftr @ X0))),
% 34.28/5.16 inference(rectify,[],[f40])).
% 34.28/5.16 thf(f351,plain,(
% 34.28/5.16 ! [X0 : n] : (((gram_L864798063lle_wf @ (gram_L1231612515_deftr @ X0))) = $true)),
% 34.28/5.16 inference(fool_elimination,[],[f350])).
% 34.28/5.16 thf(f748,plain,(
% 34.28/5.16 ~ ? [X0 : dtree] : ((gram_L646766332egular @ X0) & (((root @ X0)) = n2) & (gram_L864798063lle_wf @ X0) & (bot_bot @ set @ t = ((gram_L861583724lle_Fr @ ns @ X0))))),
% 34.28/5.16 inference(rectify,[],[f284])).
% 34.28/5.16 thf(f749,plain,(
% 34.28/5.16 ~ ? [X0 : dtree] : ((((gram_L646766332egular @ X0)) = $true) & (n2 = ((root @ X0))) & (((gram_L864798063lle_wf @ X0)) = $true) & (bot_bot @ set @ t = ((gram_L861583724lle_Fr @ ns @ X0))))),
% 34.28/5.16 inference(fool_elimination,[],[f748])).
% 34.28/5.16 thf(f750,plain,(
% 34.28/5.16 (((member @ n @ n2 @ ns)) != $true)),
% 34.28/5.16 inference(flattening,[],[f286])).
% 34.28/5.16 thf(f751,plain,(
% 34.28/5.16 ! [X0 : dtree,X1 : set @ n] : ((((member @ n @ (root @ X0) @ X1)) != $true) => (((gram_L861583724lle_Fr @ X1 @ X0)) = bot_bot @ set @ t))),
% 34.28/5.16 inference(flattening,[],[f288])).
% 34.28/5.16 thf(f780,plain,(
% 34.28/5.16 ! [X0 : dtree,X1 : set @ n] : ((((gram_L861583724lle_Fr @ X1 @ X0)) = bot_bot @ set @ t) | (((member @ n @ (root @ X0) @ X1)) = $true))),
% 34.28/5.16 inference(ennf_transformation,[],[f751])).
% 34.28/5.16 thf(f792,plain,(
% 34.28/5.16 ! [X0 : set @ n,X1 : dtree,X2 : n] : ((((gram_L1231612515_deftr @ (root @ X1))) = X1) | (((gram_L716654942_subtr @ X0 @ X1 @ (gram_L1231612515_deftr @ X2))) != $true))),
% 34.28/5.16 inference(ennf_transformation,[],[f337])).
% 34.28/5.16 thf(f985,plain,(
% 34.28/5.16 ! [X0 : dtree] : ((((gram_L646766332egular @ X0)) != $true) | (n2 != ((root @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0))))),
% 34.28/5.16 inference(ennf_transformation,[],[f749])).
% 34.28/5.16 thf(f1019,plain,(
% 34.28/5.16 (((member @ n @ n2 @ ns)) != $true)),
% 34.28/5.16 inference(cnf_transformation,[],[f750])).
% 34.28/5.16 thf(f1020,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : set @ n] : ((((gram_L861583724lle_Fr @ X1 @ X0)) = bot_bot @ set @ t) | (((member @ n @ (root @ X0) @ X1)) = $true)) )),
% 34.28/5.16 inference(cnf_transformation,[],[f780])).
% 34.28/5.16 thf(f1026,plain,(
% 34.28/5.16 (root = gram_L1905609017ubst_r)),
% 34.28/5.16 inference(cnf_transformation,[],[f8])).
% 34.28/5.16 thf(f1028,plain,(
% 34.28/5.16 (gram_L646766332egular = (^[Y0 : dtree]: (?? @ (n > dtree) @ (^[Y1 : n > dtree]: ((gram_L1918716148le_reg @ Y1 @ Y0) & (!! @ n @ (^[Y2 : n]: ((root @ (Y1 @ Y2)) = Y2))))))))),
% 34.28/5.16 inference(cnf_transformation,[],[f300])).
% 34.28/5.16 thf(f1046,plain,(
% 34.28/5.16 ( ! [X0 : n] : ((((root @ (gram_L1231612515_deftr @ X0))) = X0)) )),
% 34.28/5.16 inference(cnf_transformation,[],[f28])).
% 34.28/5.16 thf(f1051,plain,(
% 34.28/5.16 (gram_L1918716148le_reg = (^[Y0 : n > dtree]: ((^[Y1 : dtree]: (!! @ dtree @ (^[Y2 : dtree]: (!! @ set @ n @ (^[Y3 : set @ n]: ((gram_L716654942_subtr @ Y3 @ Y2 @ Y1) => ((Y0 @ (root @ Y2)) = Y2))))))))))),
% 34.28/5.16 inference(cnf_transformation,[],[f333])).
% 34.28/5.16 thf(f1053,plain,(
% 34.28/5.16 ( ! [X2 : n,X0 : set @ n,X1 : dtree] : ((((gram_L1231612515_deftr @ (root @ X1))) = X1) | (((gram_L716654942_subtr @ X0 @ X1 @ (gram_L1231612515_deftr @ X2))) != $true)) )),
% 34.28/5.16 inference(cnf_transformation,[],[f792])).
% 34.28/5.16 thf(f1060,plain,(
% 34.28/5.16 ( ! [X0 : n] : ((((gram_L864798063lle_wf @ (gram_L1231612515_deftr @ X0))) = $true)) )),
% 34.28/5.16 inference(cnf_transformation,[],[f351])).
% 34.28/5.16 thf(f1334,plain,(
% 34.28/5.16 ( ! [X0 : dtree] : ((((gram_L646766332egular @ X0)) != $true) | (n2 != ((root @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0)))) )),
% 34.28/5.16 inference(cnf_transformation,[],[f985])).
% 34.28/5.16 thf(f1340,plain,(
% 34.28/5.16 (gram_L1918716148le_reg = (^[Y0 : n > dtree]: ((^[Y1 : dtree]: (!! @ dtree @ (^[Y2 : dtree]: (!! @ set @ n @ (^[Y3 : set @ n]: ((gram_L716654942_subtr @ Y3 @ Y2 @ Y1) => ((Y0 @ (gram_L1905609017ubst_r @ Y2)) = Y2))))))))))),
% 34.28/5.16 inference(definition_unfolding,[],[f1051,f1026])).
% 34.28/5.16 thf(f1341,plain,(
% 34.28/5.16 (gram_L646766332egular = (^[Y0 : dtree]: (?? @ (n > dtree) @ (^[Y1 : n > dtree]: (((^[Y2 : n > dtree]: ((^[Y3 : dtree]: (!! @ dtree @ (^[Y4 : dtree]: (!! @ set @ n @ (^[Y5 : set @ n]: ((gram_L716654942_subtr @ Y5 @ Y4 @ Y3) => ((Y2 @ (gram_L1905609017ubst_r @ Y4)) = Y4))))))))) @ Y1 @ Y0) & (!! @ n @ (^[Y2 : n]: ((gram_L1905609017ubst_r @ (Y1 @ Y2)) = Y2))))))))),
% 34.28/5.16 inference(definition_unfolding,[],[f1028,f1340,f1026])).
% 34.28/5.16 thf(f1342,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : set @ n] : (($true = ((member @ n @ (gram_L1905609017ubst_r @ X0) @ X1))) | (((gram_L861583724lle_Fr @ X1 @ X0)) = bot_bot @ set @ t)) )),
% 34.28/5.16 inference(definition_unfolding,[],[f1020,f1026])).
% 34.28/5.16 thf(f1351,plain,(
% 34.28/5.16 ( ! [X0 : n] : ((((gram_L1905609017ubst_r @ (gram_L1231612515_deftr @ X0))) = X0)) )),
% 34.28/5.16 inference(definition_unfolding,[],[f1046,f1026])).
% 34.28/5.16 thf(f1356,plain,(
% 34.28/5.16 ( ! [X2 : n,X0 : set @ n,X1 : dtree] : ((((gram_L716654942_subtr @ X0 @ X1 @ (gram_L1231612515_deftr @ X2))) != $true) | (((gram_L1231612515_deftr @ (gram_L1905609017ubst_r @ X1))) = X1)) )),
% 34.28/5.16 inference(definition_unfolding,[],[f1053,f1026])).
% 34.28/5.16 thf(f1392,plain,(
% 34.28/5.16 ( ! [X0 : dtree] : (($true != (((^[Y0 : dtree]: (?? @ (n > dtree) @ (^[Y1 : n > dtree]: (((^[Y2 : n > dtree]: ((^[Y3 : dtree]: (!! @ dtree @ (^[Y4 : dtree]: (!! @ set @ n @ (^[Y5 : set @ n]: ((gram_L716654942_subtr @ Y5 @ Y4 @ Y3) => ((Y2 @ (gram_L1905609017ubst_r @ Y4)) = Y4))))))))) @ Y1 @ Y0) & (!! @ n @ (^[Y2 : n]: ((gram_L1905609017ubst_r @ (Y1 @ Y2)) = Y2))))))) @ X0))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0)))) )),
% 34.28/5.16 inference(definition_unfolding,[],[f1334,f1341,f1026])).
% 34.28/5.16 thf(f1406,plain,(
% 34.28/5.16 ( ! [X0 : dtree] : (($true != ((?? @ (n > dtree) @ (^[Y0 : n > dtree]: ((!! @ dtree @ (^[Y1 : dtree]: (!! @ set @ n @ (^[Y2 : set @ n]: ((gram_L716654942_subtr @ Y2 @ Y1 @ X0) => ((Y0 @ (gram_L1905609017ubst_r @ Y1)) = Y1)))))) & (!! @ n @ (^[Y1 : n]: ((gram_L1905609017ubst_r @ (Y0 @ Y1)) = Y1)))))))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0)))) )),
% 34.28/5.16 inference(beta-eta_normalization,[],[f1392])).
% 34.28/5.16 thf(f1407,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : (n > dtree)] : (($false = (((^[Y0 : n > dtree]: ((!! @ dtree @ (^[Y1 : dtree]: (!! @ set @ n @ (^[Y2 : set @ n]: ((gram_L716654942_subtr @ Y2 @ Y1 @ X0) => ((Y0 @ (gram_L1905609017ubst_r @ Y1)) = Y1)))))) & (!! @ n @ (^[Y1 : n]: ((gram_L1905609017ubst_r @ (Y0 @ Y1)) = Y1))))) @ X1))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0)))) )),
% 34.28/5.16 inference(pi_proxy_clausification,[],[f1406])).
% 34.28/5.16 thf(f1408,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : (n > dtree)] : (($false = (((!! @ dtree @ (^[Y0 : dtree]: (!! @ set @ n @ (^[Y1 : set @ n]: ((gram_L716654942_subtr @ Y1 @ Y0 @ X0) => ((X1 @ (gram_L1905609017ubst_r @ Y0)) = Y0)))))) & (!! @ n @ (^[Y0 : n]: ((gram_L1905609017ubst_r @ (X1 @ Y0)) = Y0)))))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0)))) )),
% 34.28/5.16 inference(beta-eta_normalization,[],[f1407])).
% 34.28/5.16 thf(f1409,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : (n > dtree)] : (($false = ((!! @ n @ (^[Y0 : n]: ((gram_L1905609017ubst_r @ (X1 @ Y0)) = Y0))))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0))) | ($false = ((!! @ dtree @ (^[Y0 : dtree]: (!! @ set @ n @ (^[Y1 : set @ n]: ((gram_L716654942_subtr @ Y1 @ Y0 @ X0) => ((X1 @ (gram_L1905609017ubst_r @ Y0)) = Y0))))))))) )),
% 34.28/5.16 inference(and_proxy_clausification,[],[f1408])).
% 34.28/5.16 thf(f1410,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : (n > dtree)] : (($false = (((^[Y0 : n]: ((gram_L1905609017ubst_r @ (X1 @ Y0)) = Y0)) @ (sK34 @ X1)))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0))) | ($false = ((!! @ dtree @ (^[Y0 : dtree]: (!! @ set @ n @ (^[Y1 : set @ n]: ((gram_L716654942_subtr @ Y1 @ Y0 @ X0) => ((X1 @ (gram_L1905609017ubst_r @ Y0)) = Y0))))))))) )),
% 34.28/5.16 inference(sigma_proxy_clausification,[],[f1409])).
% 34.28/5.16 thf(f1411,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : (n > dtree)] : (($false = (((^[Y0 : n]: ((gram_L1905609017ubst_r @ (X1 @ Y0)) = Y0)) @ (sK34 @ X1)))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0))) | ($false = (((^[Y0 : dtree]: (!! @ set @ n @ (^[Y1 : set @ n]: ((gram_L716654942_subtr @ Y1 @ Y0 @ X0) => ((X1 @ (gram_L1905609017ubst_r @ Y0)) = Y0))))) @ (sK35 @ X1 @ X0))))) )),
% 34.28/5.16 inference(sigma_proxy_clausification,[],[f1410])).
% 34.28/5.16 thf(f1412,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : (n > dtree)] : (($false = (((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))) = (sK34 @ X1)))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0))) | ($false = ((!! @ set @ n @ (^[Y0 : set @ n]: ((gram_L716654942_subtr @ Y0 @ (sK35 @ X1 @ X0) @ X0) => ((X1 @ (gram_L1905609017ubst_r @ (sK35 @ X1 @ X0))) = (sK35 @ X1 @ X0)))))))) )),
% 34.28/5.16 inference(beta-eta_normalization,[],[f1411])).
% 34.28/5.16 thf(f1413,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : (n > dtree)] : ((((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0))) | ($false = ((!! @ set @ n @ (^[Y0 : set @ n]: ((gram_L716654942_subtr @ Y0 @ (sK35 @ X1 @ X0) @ X0) => ((X1 @ (gram_L1905609017ubst_r @ (sK35 @ X1 @ X0))) = (sK35 @ X1 @ X0)))))))) )),
% 34.28/5.16 inference(equality_proxy_clausification,[],[f1412])).
% 34.28/5.16 thf(f1414,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : (n > dtree)] : ((((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0))) | ($false = (((^[Y0 : set @ n]: ((gram_L716654942_subtr @ Y0 @ (sK35 @ X1 @ X0) @ X0) => ((X1 @ (gram_L1905609017ubst_r @ (sK35 @ X1 @ X0))) = (sK35 @ X1 @ X0)))) @ (sK36 @ X1 @ X0))))) )),
% 34.28/5.16 inference(sigma_proxy_clausification,[],[f1413])).
% 34.28/5.16 thf(f1415,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : (n > dtree)] : ((((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0))) | ($false = (((gram_L716654942_subtr @ (sK36 @ X1 @ X0) @ (sK35 @ X1 @ X0) @ X0) => ((X1 @ (gram_L1905609017ubst_r @ (sK35 @ X1 @ X0))) = (sK35 @ X1 @ X0)))))) )),
% 34.28/5.16 inference(beta-eta_normalization,[],[f1414])).
% 34.28/5.16 thf(f1416,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : (n > dtree)] : ((((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0))) | ($false = (((X1 @ (gram_L1905609017ubst_r @ (sK35 @ X1 @ X0))) = (sK35 @ X1 @ X0))))) )),
% 34.28/5.16 inference(imp_proxy_clausification,[],[f1415])).
% 34.28/5.16 thf(f1417,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : (n > dtree)] : ((bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | ($true = ((gram_L716654942_subtr @ (sK36 @ X1 @ X0) @ (sK35 @ X1 @ X0) @ X0)))) )),
% 34.28/5.16 inference(imp_proxy_clausification,[],[f1415])).
% 34.28/5.16 thf(f1418,plain,(
% 34.28/5.16 ( ! [X0 : dtree,X1 : (n > dtree)] : ((bot_bot @ set @ t != ((gram_L861583724lle_Fr @ ns @ X0))) | (n2 != ((gram_L1905609017ubst_r @ X0))) | (((gram_L864798063lle_wf @ X0)) != $true) | (((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | (((sK35 @ X1 @ X0)) != ((X1 @ (gram_L1905609017ubst_r @ (sK35 @ X1 @ X0)))))) )),
% 34.28/5.16 inference(equality_proxy_clausification,[],[f1416])).
% 34.28/5.16 thf(f3076,plain,(
% 34.28/5.16 ( ! [X0 : n,X1 : set @ n] : ((bot_bot @ set @ t = ((gram_L861583724lle_Fr @ X1 @ (gram_L1231612515_deftr @ X0)))) | (((member @ n @ X0 @ X1)) = $true)) )),
% 34.28/5.16 inference(constrained_superposition,[],[f1342,f1351])).
% 34.28/5.16 thf(f14662,plain,(
% 34.28/5.16 ( ! [X0 : n,X1 : (n > dtree)] : ((bot_bot @ set @ t != bot_bot @ set @ t) | (n2 != ((gram_L1905609017ubst_r @ (gram_L1231612515_deftr @ X0)))) | (((gram_L864798063lle_wf @ (gram_L1231612515_deftr @ X0))) != $true) | (((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | ($true = ((gram_L716654942_subtr @ (sK36 @ X1 @ (gram_L1231612515_deftr @ X0)) @ (sK35 @ X1 @ (gram_L1231612515_deftr @ X0)) @ (gram_L1231612515_deftr @ X0)))) | ($true = ((member @ n @ X0 @ ns)))) )),
% 34.28/5.16 inference(constrained_superposition,[],[f1417,f3076])).
% 34.28/5.16 thf(f14663,plain,(
% 34.28/5.16 ( ! [X0 : n,X1 : (n > dtree)] : ((bot_bot @ set @ t != bot_bot @ set @ t) | (n2 != ((gram_L1905609017ubst_r @ (gram_L1231612515_deftr @ X0)))) | (((gram_L864798063lle_wf @ (gram_L1231612515_deftr @ X0))) != $true) | (((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | (((sK35 @ X1 @ (gram_L1231612515_deftr @ X0))) != ((X1 @ (gram_L1905609017ubst_r @ (sK35 @ X1 @ (gram_L1231612515_deftr @ X0)))))) | ($true = ((member @ n @ X0 @ ns)))) )),
% 34.28/5.16 inference(constrained_superposition,[],[f1418,f3076])).
% 34.28/5.16 thf(f14669,plain,(
% 34.28/5.16 ( ! [X0 : n,X1 : (n > dtree)] : ((n2 != ((gram_L1905609017ubst_r @ (gram_L1231612515_deftr @ X0)))) | (((gram_L864798063lle_wf @ (gram_L1231612515_deftr @ X0))) != $true) | (((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | (((sK35 @ X1 @ (gram_L1231612515_deftr @ X0))) != ((X1 @ (gram_L1905609017ubst_r @ (sK35 @ X1 @ (gram_L1231612515_deftr @ X0)))))) | ($true = ((member @ n @ X0 @ ns)))) )),
% 34.28/5.16 inference(trivial_inequality_removal,[],[f14663])).
% 34.28/5.16 thf(f14670,plain,(
% 34.28/5.16 ( ! [X0 : n,X1 : (n > dtree)] : ((n2 != ((gram_L1905609017ubst_r @ (gram_L1231612515_deftr @ X0)))) | (((gram_L864798063lle_wf @ (gram_L1231612515_deftr @ X0))) != $true) | (((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | ($true = ((gram_L716654942_subtr @ (sK36 @ X1 @ (gram_L1231612515_deftr @ X0)) @ (sK35 @ X1 @ (gram_L1231612515_deftr @ X0)) @ (gram_L1231612515_deftr @ X0)))) | ($true = ((member @ n @ X0 @ ns)))) )),
% 34.28/5.16 inference(trivial_inequality_removal,[],[f14662])).
% 34.28/5.16 thf(f14671,plain,(
% 34.28/5.16 ( ! [X0 : n,X1 : (n > dtree)] : ((n2 != ((gram_L1905609017ubst_r @ (gram_L1231612515_deftr @ X0)))) | (((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | (((sK35 @ X1 @ (gram_L1231612515_deftr @ X0))) != ((X1 @ (gram_L1905609017ubst_r @ (sK35 @ X1 @ (gram_L1231612515_deftr @ X0)))))) | ($true = ((member @ n @ X0 @ ns)))) )),
% 34.28/5.16 inference(forward_subsumption_resolution,[],[f14669,f1060])).
% 34.28/5.16 thf(f14672,plain,(
% 34.28/5.16 ( ! [X0 : n,X1 : (n > dtree)] : ((n2 != ((gram_L1905609017ubst_r @ (gram_L1231612515_deftr @ X0)))) | (((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | ($true = ((gram_L716654942_subtr @ (sK36 @ X1 @ (gram_L1231612515_deftr @ X0)) @ (sK35 @ X1 @ (gram_L1231612515_deftr @ X0)) @ (gram_L1231612515_deftr @ X0)))) | ($true = ((member @ n @ X0 @ ns)))) )),
% 34.28/5.16 inference(forward_subsumption_resolution,[],[f14670,f1060])).
% 34.28/5.16 thf(f14673,plain,(
% 34.28/5.16 ( ! [X0 : n,X1 : (n > dtree)] : ((((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | (n2 != X0) | (((sK35 @ X1 @ (gram_L1231612515_deftr @ X0))) != ((X1 @ (gram_L1905609017ubst_r @ (sK35 @ X1 @ (gram_L1231612515_deftr @ X0)))))) | ($true = ((member @ n @ X0 @ ns)))) )),
% 34.28/5.16 inference(forward_demodulation,[],[f14671,f1351])).
% 34.28/5.16 thf(f14674,plain,(
% 34.28/5.16 ( ! [X0 : n,X1 : (n > dtree)] : ((((sK34 @ X1)) != ((gram_L1905609017ubst_r @ (X1 @ (sK34 @ X1))))) | (n2 != X0) | ($true = ((gram_L716654942_subtr @ (sK36 @ X1 @ (gram_L1231612515_deftr @ X0)) @ (sK35 @ X1 @ (gram_L1231612515_deftr @ X0)) @ (gram_L1231612515_deftr @ X0)))) | ($true = ((member @ n @ X0 @ ns)))) )),
% 34.28/5.16 inference(forward_demodulation,[],[f14672,f1351])).
% 34.28/5.16 thf(f14683,plain,(
% 34.28/5.16 ( ! [X2 : n,X0 : n,X1 : (n > n)] : ((((sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0))))) != X0) | (n2 != X2) | (((sK35 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0))) @ (gram_L1231612515_deftr @ X2))) != (((^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0))) @ (gram_L1905609017ubst_r @ (sK35 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0))) @ (gram_L1231612515_deftr @ X2)))))) | ($true = ((member @ n @ X2 @ ns))) | (((X1 @ (sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0)))))) != X0)) )),
% 34.28/5.16 inference(constrained_superposition,[],[f14673,f1351])).
% 34.28/5.16 thf(f14702,plain,(
% 34.28/5.16 ( ! [X2 : n,X0 : n,X1 : (n > n)] : ((((sK35 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0))) @ (gram_L1231612515_deftr @ X2))) != ((gram_L1231612515_deftr @ (X1 @ (gram_L1905609017ubst_r @ (sK35 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0))) @ (gram_L1231612515_deftr @ X2))))))) | (n2 != X2) | (((sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0))))) != X0) | ($true = ((member @ n @ X2 @ ns))) | (((X1 @ (sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0)))))) != X0)) )),
% 34.28/5.16 inference(beta-eta_normalization,[],[f14683])).
% 34.28/5.16 thf(f14835,plain,(
% 34.28/5.16 ( ! [X2 : n,X0 : n,X1 : (n > n)] : ((n2 != X2) | (((sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0))))) != X0) | ($true = ((gram_L716654942_subtr @ (sK36 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0))) @ (gram_L1231612515_deftr @ X2)) @ (sK35 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0))) @ (gram_L1231612515_deftr @ X2)) @ (gram_L1231612515_deftr @ X2)))) | ($true = ((member @ n @ X2 @ ns))) | (((X1 @ (sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X1 @ Y0)))))) != X0)) )),
% 34.28/5.16 inference(constrained_superposition,[],[f14674,f1351])).
% 34.28/5.16 thf(f16612,plain,(
% 34.28/5.16 ( ! [X0 : (n > n),X1 : n] : ((((sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X0 @ Y0))))) != X1) | ($true = ((gram_L716654942_subtr @ (sK36 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X0 @ Y0))) @ (gram_L1231612515_deftr @ n2)) @ (sK35 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X0 @ Y0))) @ (gram_L1231612515_deftr @ n2)) @ (gram_L1231612515_deftr @ n2)))) | (((member @ n @ n2 @ ns)) = $true) | (((X0 @ (sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X0 @ Y0)))))) != X1)) )),
% 34.28/5.16 inference(equality_resolution,[],[f14835])).
% 34.28/5.16 thf(f16613,plain,(
% 34.28/5.16 ( ! [X0 : (n > n),X1 : n] : ((((sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X0 @ Y0))))) != X1) | ($true = ((gram_L716654942_subtr @ (sK36 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X0 @ Y0))) @ (gram_L1231612515_deftr @ n2)) @ (sK35 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X0 @ Y0))) @ (gram_L1231612515_deftr @ n2)) @ (gram_L1231612515_deftr @ n2)))) | (((X0 @ (sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X0 @ Y0)))))) != X1)) )),
% 34.28/5.16 inference(forward_subsumption_resolution,[],[f16612,f1019])).
% 34.28/5.16 thf(f16659,plain,(
% 34.28/5.16 ( ! [X0 : (n > n)] : ((((sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X0 @ Y0))))) != ((X0 @ (sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X0 @ Y0))))))) | ($true = ((gram_L716654942_subtr @ (sK36 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X0 @ Y0))) @ (gram_L1231612515_deftr @ n2)) @ (sK35 @ (^[Y0 : n]: (gram_L1231612515_deftr @ (X0 @ Y0))) @ (gram_L1231612515_deftr @ n2)) @ (gram_L1231612515_deftr @ n2))))) )),
% 34.28/5.16 inference(equality_resolution,[],[f16613])).
% 34.28/5.16 thf(f16723,plain,(
% 34.28/5.16 ($true = ((gram_L716654942_subtr @ (sK36 @ (^[Y0 : n]: (gram_L1231612515_deftr @ ((^[Y1 : n]: (Y1)) @ Y0))) @ (gram_L1231612515_deftr @ n2)) @ (sK35 @ (^[Y0 : n]: (gram_L1231612515_deftr @ ((^[Y1 : n]: (Y1)) @ Y0))) @ (gram_L1231612515_deftr @ n2)) @ (gram_L1231612515_deftr @ n2))))),
% 34.28/5.16 inference(equality_resolution,[],[f16659])).
% 34.28/5.16 thf(f16726,plain,(
% 34.28/5.16 ($true = ((gram_L716654942_subtr @ (sK36 @ gram_L1231612515_deftr @ (gram_L1231612515_deftr @ n2)) @ (sK35 @ gram_L1231612515_deftr @ (gram_L1231612515_deftr @ n2)) @ (gram_L1231612515_deftr @ n2))))),
% 34.28/5.16 inference(beta-eta_normalization,[],[f16723])).
% 34.28/5.16 thf(f16797,plain,(
% 34.28/5.16 ($true != $true) | (((sK35 @ gram_L1231612515_deftr @ (gram_L1231612515_deftr @ n2))) = ((gram_L1231612515_deftr @ (gram_L1905609017ubst_r @ (sK35 @ gram_L1231612515_deftr @ (gram_L1231612515_deftr @ n2))))))),
% 34.28/5.16 inference(constrained_superposition,[],[f1356,f16726])).
% 34.28/5.16 thf(f16804,plain,(
% 34.28/5.16 (((sK35 @ gram_L1231612515_deftr @ (gram_L1231612515_deftr @ n2))) = ((gram_L1231612515_deftr @ (gram_L1905609017ubst_r @ (sK35 @ gram_L1231612515_deftr @ (gram_L1231612515_deftr @ n2))))))),
% 34.28/5.16 inference(trivial_inequality_removal,[],[f16797])).
% 34.28/5.16 thf(f17293,plain,(
% 34.28/5.16 ( ! [X0 : n] : ((((sK35 @ (^[Y0 : n]: (gram_L1231612515_deftr @ ((^[Y1 : n]: (Y1)) @ Y0))) @ (gram_L1231612515_deftr @ n2))) != ((sK35 @ gram_L1231612515_deftr @ (gram_L1231612515_deftr @ n2)))) | (n2 != n2) | (((sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ ((^[Y1 : n]: (Y1)) @ Y0))))) != X0) | (((member @ n @ n2 @ ns)) = $true) | ((((^[Y0 : n]: (Y0)) @ (sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ ((^[Y1 : n]: (Y1)) @ Y0)))))) != X0)) )),
% 34.28/5.16 inference(constrained_superposition,[],[f14702,f16804])).
% 34.28/5.16 thf(f17349,plain,(
% 34.28/5.16 ( ! [X0 : n] : ((((sK35 @ (^[Y0 : n]: (gram_L1231612515_deftr @ ((^[Y1 : n]: (Y1)) @ Y0))) @ (gram_L1231612515_deftr @ n2))) != ((sK35 @ gram_L1231612515_deftr @ (gram_L1231612515_deftr @ n2)))) | (((sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ ((^[Y1 : n]: (Y1)) @ Y0))))) != X0) | (((member @ n @ n2 @ ns)) = $true) | ((((^[Y0 : n]: (Y0)) @ (sK34 @ (^[Y0 : n]: (gram_L1231612515_deftr @ ((^[Y1 : n]: (Y1)) @ Y0)))))) != X0)) )),
% 34.28/5.16 inference(trivial_inequality_removal,[],[f17293])).
% 34.28/5.16 thf(f17350,plain,(
% 34.28/5.16 ( ! [X0 : n] : ((((sK35 @ gram_L1231612515_deftr @ (gram_L1231612515_deftr @ n2))) != ((sK35 @ gram_L1231612515_deftr @ (gram_L1231612515_deftr @ n2)))) | (((sK34 @ gram_L1231612515_deftr)) != X0) | (((member @ n @ n2 @ ns)) = $true) | (((sK34 @ gram_L1231612515_deftr)) != X0)) )),
% 34.28/5.16 inference(beta-eta_normalization,[],[f17349])).
% 34.28/5.16 thf(f17351,plain,(
% 34.28/5.16 ( ! [X0 : n] : ((((sK35 @ gram_L1231612515_deftr @ (gram_L1231612515_deftr @ n2))) != ((sK35 @ gram_L1231612515_deftr @ (gram_L1231612515_deftr @ n2)))) | (((sK34 @ gram_L1231612515_deftr)) != X0) | (((member @ n @ n2 @ ns)) = $true)) )),
% 34.28/5.16 inference(duplicate_literal_removal,[],[f17350])).
% 34.28/5.16 thf(f17352,plain,(
% 34.28/5.16 ( ! [X0 : n] : ((((sK34 @ gram_L1231612515_deftr)) != X0) | (((member @ n @ n2 @ ns)) = $true)) )),
% 34.28/5.16 inference(trivial_inequality_removal,[],[f17351])).
% 34.28/5.16 thf(f17363,plain,(
% 34.28/5.16 ( ! [X0 : n] : ((((sK34 @ gram_L1231612515_deftr)) != X0)) )),
% 34.28/5.16 inference(forward_subsumption_resolution,[],[f17352,f1019])).
% 34.28/5.16 thf(f17418,plain,(
% 34.28/5.16 $false),
% 34.28/5.16 inference(equality_resolution,[],[f17363])).
% 34.28/5.16 % SZS output end Proof for theBenchmark
% 34.28/5.16 % (1629808)------------------------------
% 34.28/5.16 % (1629808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.28/5.16 % (1629808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.28/5.16 % (1629808)CaDiCaL version: 2.1.3
% 34.28/5.16 % (1629808)Termination reason: Refutation
% 34.28/5.16 % (1629808)Time elapsed: 1.642 s
% 34.28/5.16 % (1629808)Peak memory usage: 27 MB
% 34.28/5.16 % (1629808)Instructions burned: 3155 (million)
% 34.28/5.16 % (1629713)Success in time 4.934 s
% 34.28/5.16 % Vampire exiting
%------------------------------------------------------------------------------