%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR077+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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 : Tue Sep 29 09:44:59 AM UTC 2026
% Result : Theorem 12.66s 4.16s
% Output : Refutation 12.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR077+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.17 % Computer : n003.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Mon Sep 28 22:28:43 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.20 Running first-order model finding
% 0.07/0.20 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.23/2.01 % (2106512)Will run a generic schedule for satisfiability detection.
% 8.23/2.01 % (2106519)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1663818523:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 8.23/2.01 % (2106518)% WARNING: option uhcvi not known.
% 8.23/2.01 % (2106517)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2480336372_2997 on theBenchmark for (2997ds/0Mi)
% 8.23/2.01 % (2106518)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2247550677:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 8.23/2.01 % (2106520)dis+10_1_sil=32000:sp=arity:random_seed=1830125720:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 8.23/2.01 % (2106521)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3355738639:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 8.23/2.01 % (2106522)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1802522810:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 8.23/2.01 % (2106523)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2648497125:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 8.23/2.01 % (2106520)Instruction limit reached!
% 8.23/2.01 % (2106520)------------------------------
% 8.23/2.01 % (2106520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.23/2.01 % (2106520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.23/2.01 % (2106520)CaDiCaL version: 2.1.3
% 8.23/2.01 % (2106520)Termination reason: Instruction limit
% 8.23/2.01 % (2106520)Termination phase: Preprocessing 3
% 8.23/2.01 % (2106520)Time elapsed: 0.067 s
% 8.23/2.01 % (2106520)Peak memory usage: 29 MB
% 8.23/2.01 % (2106520)Instructions burned: 104 (million)
% 8.23/2.01 % (2106521)Instruction limit reached!
% 8.23/2.01 % (2106521)------------------------------
% 8.23/2.01 % (2106521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.23/2.01 % (2106521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.23/2.01 % (2106521)CaDiCaL version: 2.1.3
% 8.23/2.01 % (2106521)Termination reason: Instruction limit
% 8.23/2.01 % (2106521)Termination phase: NewCNF
% 8.23/2.01 % (2106521)Time elapsed: 0.079 s
% 8.23/2.01 % (2106521)Peak memory usage: 32 MB
% 8.23/2.01 % (2106521)Instructions burned: 116 (million)
% 8.23/2.01 % (2106522)Instruction limit reached!
% 8.23/2.01 % (2106522)------------------------------
% 8.23/2.01 % (2106522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.23/2.01 % (2106522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.23/2.01 % (2106522)CaDiCaL version: 2.1.3
% 8.23/2.01 % (2106522)Termination reason: Instruction limit
% 8.23/2.01 % (2106522)Termination phase: Clausification
% 8.23/2.01 % (2106522)Time elapsed: 0.082 s
% 8.23/2.01 % (2106522)Peak memory usage: 31 MB
% 8.23/2.01 % (2106522)Instructions burned: 132 (million)
% 8.23/2.01 % (2106531)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=588370421:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi)
% 8.23/2.01 % (2106523)Instruction limit reached!
% 8.23/2.01 % (2106523)------------------------------
% 8.23/2.01 % (2106523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.23/2.01 % (2106523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.23/2.01 % (2106523)CaDiCaL version: 2.1.3
% 8.23/2.01 % (2106523)Termination reason: Instruction limit
% 8.23/2.01 % (2106523)Termination phase: Property scanning
% 8.23/2.01 % (2106523)Time elapsed: 0.096 s
% 8.23/2.01 % (2106523)Peak memory usage: 31 MB
% 8.23/2.01 % (2106523)Instructions burned: 159 (million)
% 8.23/2.01 % (2106532)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3097559042:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 8.23/2.01 % (2106533)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=4286024398:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 8.23/2.01 % (2106535)ott-21_1_sil=16000:fs=off:random_seed=644007677:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 8.23/2.01 % (2106532)Instruction limit reached!
% 8.23/2.01 % (2106532)------------------------------
% 8.23/2.01 % (2106532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.23/2.01 % (2106532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/3.12 % (2106532)CaDiCaL version: 2.1.3
% 18.38/3.12 % (2106532)Termination reason: Instruction limit
% 18.38/3.12 % (2106532)Termination phase: Clausification
% 18.38/3.12 % (2106532)Time elapsed: 0.075 s
% 18.38/3.12 % (2106532)Peak memory usage: 31 MB
% 18.38/3.12 % (2106532)Instructions burned: 132 (million)
% 18.38/3.12 % (2106539)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2045529692:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi)
% 18.38/3.12 % (2106535)Instruction limit reached!
% 18.38/3.12 % (2106535)------------------------------
% 18.38/3.12 % (2106535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.38/3.12 % (2106535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/3.12 % (2106535)CaDiCaL version: 2.1.3
% 18.38/3.12 % (2106535)Termination reason: Instruction limit
% 18.38/3.12 % (2106535)Termination phase: Property scanning
% 18.38/3.12 % (2106535)Time elapsed: 0.103 s
% 18.38/3.12 % (2106535)Peak memory usage: 31 MB
% 18.38/3.12 % (2106535)Instructions burned: 180 (million)
% 18.38/3.12 % (2106541)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3713375667:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 18.38/3.12 % (2106533)Instruction limit reached!
% 18.38/3.12 % (2106533)------------------------------
% 18.38/3.12 % (2106533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.38/3.12 % (2106533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/3.12 % (2106533)CaDiCaL version: 2.1.3
% 18.38/3.12 % (2106533)Termination reason: Instruction limit
% 18.38/3.12 % (2106533)Termination phase: Saturation
% 18.38/3.12 % (2106533)Time elapsed: 0.330 s
% 18.38/3.12 % (2106533)Peak memory usage: 40 MB
% 18.38/3.12 % (2106533)Instructions burned: 685 (million)
% 18.38/3.12 % (2106539)Instruction limit reached!
% 18.38/3.12 % (2106539)------------------------------
% 18.38/3.12 % (2106539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.38/3.12 % (2106539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/3.12 % (2106539)CaDiCaL version: 2.1.3
% 18.38/3.12 % (2106539)Termination reason: Instruction limit
% 18.38/3.12 % (2106539)Termination phase: Saturation
% 18.38/3.12 % (2106539)Time elapsed: 0.237 s
% 18.38/3.12 % (2106539)Peak memory usage: 35 MB
% 18.38/3.12 % (2106539)Instructions burned: 479 (million)
% 18.38/3.12 % (2106531)Instruction limit reached!
% 18.38/3.12 % (2106531)------------------------------
% 18.38/3.12 % (2106531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.38/3.12 % (2106531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/3.12 % (2106531)CaDiCaL version: 2.1.3
% 18.38/3.12 % (2106531)Termination reason: Instruction limit
% 18.38/3.12 % (2106531)Termination phase: Finite model building preprocessing
% 18.38/3.12 % (2106531)Time elapsed: 0.347 s
% 18.38/3.12 % (2106531)Peak memory usage: 42 MB
% 18.38/3.12 % (2106531)Instructions burned: 716 (million)
% 18.38/3.12 % (2106543)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3359795829:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 18.38/3.12 % (2106544)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1367178143:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 18.38/3.12 % (2106545)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=3816142814:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 18.38/3.12 % (2106541)Instruction limit reached!
% 18.38/3.12 % (2106541)------------------------------
% 18.38/3.12 % (2106541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.38/3.12 % (2106541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/3.12 % (2106541)CaDiCaL version: 2.1.3
% 18.38/3.12 % (2106541)Termination reason: Instruction limit
% 18.38/3.12 % (2106541)Termination phase: Finite model building preprocessing
% 18.38/3.12 % (2106541)Time elapsed: 0.419 s
% 18.38/3.12 % (2106541)Peak memory usage: 46 MB
% 18.38/3.12 % (2106541)Instructions burned: 867 (million)
% 18.38/3.12 % (2106549)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2288969035:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 18.38/3.12 % (2106545)Instruction limit reached!
% 18.38/3.12 % (2106545)------------------------------
% 18.38/3.12 % (2106545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.38/3.12 % (2106545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.14 % (2106545)CaDiCaL version: 2.1.3
% 12.66/4.14 % (2106545)Termination reason: Instruction limit
% 12.66/4.14 % (2106545)Termination phase: Saturation
% 12.66/4.14 % (2106545)Time elapsed: 0.349 s
% 12.66/4.14 % (2106545)Peak memory usage: 42 MB
% 12.66/4.14 % (2106545)Instructions burned: 693 (million)
% 12.66/4.14 % (2106551)fmb+10_1_sil=64000:random_seed=815489181:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 12.66/4.14 % (2106544)Instruction limit reached!
% 12.66/4.14 % (2106544)------------------------------
% 12.66/4.14 % (2106544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.14 % (2106544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.14 % (2106544)CaDiCaL version: 2.1.3
% 12.66/4.14 % (2106544)Termination reason: Instruction limit
% 12.66/4.14 % (2106544)Termination phase: Finite model building preprocessing
% 12.66/4.14 % (2106544)Time elapsed: 0.420 s
% 12.66/4.14 % (2106544)Peak memory usage: 47 MB
% 12.66/4.14 % (2106544)Instructions burned: 890 (million)
% 12.66/4.14 % Detected minimum model sizes of [51]
% 12.66/4.14 % Detected maximum model sizes of [max]
% 12.66/4.14 % (2106517)Cannot represent all propositional literals internally
% 12.66/4.14 % (2106517)Refutation not found, incomplete strategy
% 12.66/4.14 % (2106517)------------------------------
% 12.66/4.14 % (2106517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.14 % (2106517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.14 % (2106517)CaDiCaL version: 2.1.3
% 12.66/4.14 % (2106517)Termination reason: Refutation not found, incomplete strategy
% 12.66/4.14 % (2106517)Time elapsed: 0.900 s
% 12.66/4.14 % (2106517)Peak memory usage: 61 MB
% 12.66/4.14 % (2106517)Instructions burned: 1881 (million)
% 12.66/4.14 % (2106553)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=223440942:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 12.66/4.14 % (2106517)------------------------------
% 12.66/4.14 % (2106517)------------------------------
% 12.66/4.14 % (2106555)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1242269507:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 12.66/4.14 % (2106543)Instruction limit reached!
% 12.66/4.14 % (2106543)------------------------------
% 12.66/4.14 % (2106543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.14 % (2106543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.14 % (2106543)CaDiCaL version: 2.1.3
% 12.66/4.14 % (2106543)Termination reason: Instruction limit
% 12.66/4.14 % (2106543)Termination phase: Saturation
% 12.66/4.14 % (2106543)Time elapsed: 0.606 s
% 12.66/4.14 % (2106543)Peak memory usage: 44 MB
% 12.66/4.14 % (2106543)Instructions burned: 1181 (million)
% 12.66/4.14 % (2106557)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=928734074:i=5131_2986 on theBenchmark for (2986ds/5131Mi)
% 12.66/4.14 % (2106549)Instruction limit reached!
% 12.66/4.14 % (2106549)------------------------------
% 12.66/4.14 % (2106549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.14 % (2106549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.14 % (2106549)CaDiCaL version: 2.1.3
% 12.66/4.14 % (2106549)Termination reason: Instruction limit
% 12.66/4.14 % (2106549)Termination phase: Saturation
% 12.66/4.14 % (2106549)Time elapsed: 0.423 s
% 12.66/4.14 % (2106549)Peak memory usage: 44 MB
% 12.66/4.14 % (2106549)Instructions burned: 882 (million)
% 12.66/4.14 % (2106559)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1617535040:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 12.66/4.14 % (2106555)Instruction limit reached!
% 12.66/4.14 % (2106555)------------------------------
% 12.66/4.14 % (2106555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.14 % (2106555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.14 % (2106555)CaDiCaL version: 2.1.3
% 12.66/4.14 % (2106555)Termination reason: Instruction limit
% 12.66/4.14 % (2106555)Termination phase: Finite model building preprocessing
% 12.66/4.14 % (2106555)Time elapsed: 0.440 s
% 12.66/4.14 % (2106555)Peak memory usage: 46 MB
% 12.66/4.14 % (2106555)Instructions burned: 920 (million)
% 12.66/4.14 % (2106561)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3086120878:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 12.66/4.14 % Detected minimum model sizes of [51]
% 12.66/4.14 % Detected maximum model sizes of [max]
% 12.66/4.14 % (2106551)Cannot represent all propositional literals internally
% 12.66/4.14 % (2106551)Refutation not found, incomplete strategy
% 12.66/4.14 % (2106551)------------------------------
% 12.66/4.14 % (2106551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.14 % (2106551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.14 % (2106551)CaDiCaL version: 2.1.3
% 12.66/4.14 % (2106551)Termination reason: Refutation not found, incomplete strategy
% 12.66/4.14 % (2106551)Time elapsed: 0.664 s
% 12.66/4.14 % (2106551)Peak memory usage: 51 MB
% 12.66/4.14 % (2106551)Instructions burned: 1452 (million)
% 12.66/4.14 % (2106551)------------------------------
% 12.66/4.14 % (2106551)------------------------------
% 12.66/4.14 % (2106563)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=325279350:fmbsr=2.30978:i=2174_2981 on theBenchmark for (2981ds/2174Mi)
% 12.66/4.14 % Detected minimum model sizes of [51]
% 12.66/4.14 % Detected maximum model sizes of [max]
% 12.66/4.14 % (2106553)Cannot represent all propositional literals internally
% 12.66/4.14 % (2106553)Refutation not found, incomplete strategy
% 12.66/4.14 % (2106553)------------------------------
% 12.66/4.14 % (2106553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.14 % (2106553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.14 % (2106553)CaDiCaL version: 2.1.3
% 12.66/4.14 % (2106553)Termination reason: Refutation not found, incomplete strategy
% 12.66/4.14 % (2106553)Time elapsed: 0.697 s
% 12.66/4.14 % (2106553)Peak memory usage: 52 MB
% 12.66/4.14 % (2106553)Instructions burned: 1527 (million)
% 12.66/4.14 % (2106553)------------------------------
% 12.66/4.14 % (2106553)------------------------------
% 12.66/4.14 % (2106565)ott-2_1_sil=16000:newcnf=on:random_seed=2995507235:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2980 on theBenchmark for (2980ds/869Mi)
% 12.66/4.14 % (2106559)Instruction limit reached!
% 12.66/4.14 % (2106559)------------------------------
% 12.66/4.14 % (2106559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.14 % (2106559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.14 % (2106559)CaDiCaL version: 2.1.3
% 12.66/4.14 % (2106559)Termination reason: Instruction limit
% 12.66/4.14 % (2106559)Termination phase: Saturation
% 12.66/4.14 % (2106559)Time elapsed: 0.771 s
% 12.66/4.14 % (2106559)Peak memory usage: 49 MB
% 12.66/4.14 % (2106559)Instructions burned: 1472 (million)
% 12.66/4.14 % (2106567)ott+10_1_sil=32000:tgt=ground:random_seed=3533646456:i=5114:av=off_2977 on theBenchmark for (2977ds/5114Mi)
% 12.66/4.14 % (2106565)Instruction limit reached!
% 12.66/4.14 % (2106565)------------------------------
% 12.66/4.14 % (2106565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.14 % (2106565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.14 % (2106565)CaDiCaL version: 2.1.3
% 12.66/4.14 % (2106565)Termination reason: Instruction limit
% 12.66/4.14 % (2106565)Termination phase: Saturation
% 12.66/4.14 % (2106565)Time elapsed: 0.441 s
% 12.66/4.14 % (2106565)Peak memory usage: 43 MB
% 12.66/4.14 % (2106565)Instructions burned: 869 (million)
% 12.66/4.14 % (2106569)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3909441807:i=54282_2975 on theBenchmark for (2975ds/54282Mi)
% 12.66/4.14 % Detected minimum model sizes of [51]
% 12.66/4.14 % Detected maximum model sizes of [max]
% 12.66/4.14 % (2106561)Cannot represent all propositional literals internally
% 12.66/4.14 % (2106561)Refutation not found, incomplete strategy
% 12.66/4.14 % (2106561)------------------------------
% 12.66/4.14 % (2106561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.14 % (2106561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.14 % (2106561)CaDiCaL version: 2.1.3
% 12.66/4.14 % (2106561)Termination reason: Refutation not found, incomplete strategy
% 12.66/4.14 % (2106561)Time elapsed: 0.881 s
% 12.66/4.14 % (2106561)Peak memory usage: 58 MB
% 12.66/4.14 % (2106561)Instructions burned: 1850 (million)
% 12.66/4.14 % (2106561)------------------------------
% 12.66/4.14 % (2106561)------------------------------
% 12.66/4.14 % (2106571)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3078609355:i=3512:aac=none_2973 on theBenchmark for (2973ds/3512Mi)
% 12.66/4.14 % (2106563)Instruction limit reached!
% 12.66/4.14 % (2106563)------------------------------
% 12.66/4.14 % (2106563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.14 % (2106563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.16 % (2106563)CaDiCaL version: 2.1.3
% 12.66/4.16 % (2106563)Termination reason: Instruction limit
% 12.66/4.16 % (2106563)Termination phase: Finite model building preprocessing
% 12.66/4.16 % (2106563)Time elapsed: 1.056 s
% 12.66/4.16 % (2106563)Peak memory usage: 71 MB
% 12.66/4.16 % (2106563)Instructions burned: 2174 (million)
% 12.66/4.16 % (2106573)dis+21_1_sil=32000:sas=cadical:random_seed=3530674482:i=3773:amm=off_2970 on theBenchmark for (2970ds/3773Mi)
% 12.66/4.16 % Detected minimum model sizes of [51]
% 12.66/4.16 % Detected maximum model sizes of [max]
% 12.66/4.16 % (2106569)Cannot represent all propositional literals internally
% 12.66/4.16 % (2106569)Refutation not found, incomplete strategy
% 12.66/4.16 % (2106569)------------------------------
% 12.66/4.16 % (2106569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.16 % (2106569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.16 % (2106569)CaDiCaL version: 2.1.3
% 12.66/4.16 % (2106569)Termination reason: Refutation not found, incomplete strategy
% 12.66/4.16 % (2106569)Time elapsed: 0.892 s
% 12.66/4.16 % (2106569)Peak memory usage: 60 MB
% 12.66/4.16 % (2106569)Instructions burned: 1874 (million)
% 12.66/4.16 % (2106569)------------------------------
% 12.66/4.16 % (2106569)------------------------------
% 12.66/4.16 % (2106575)ott+11_1_sil=16000:gs=on:random_seed=2772620629:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2966 on theBenchmark for (2966ds/2251Mi)
% 12.66/4.16 % (2106573) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2106512-2106573"...
% 12.66/4.16 % (2106573)...printing done.
% 12.66/4.16 % (2106573)Refutation found. Thanks to Tanya!
% 12.66/4.16 % SZS status Theorem for theBenchmark
% 12.66/4.16 % SZS output start Proof for theBenchmark
% 12.66/4.16 fof(f26,axiom,(
% 12.66/4.16 ! [X0,X1] : (s__subclass(X0,X1) => (s__instance(X0,s__SetOrClass) & s__instance(X1,s__SetOrClass)))),
% 12.66/4.16 file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_26)).
% 12.66/4.16 fof(f27,axiom,(
% 12.66/4.16 ! [X0,X1,X2] : ((s__instance(X1,s__SetOrClass) & s__instance(X0,s__SetOrClass)) => ((s__subclass(X0,X1) & s__instance(X2,X0)) => s__instance(X2,X1)))),
% 12.66/4.16 file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_27)).
% 12.66/4.16 fof(f846,axiom,(
% 12.66/4.16 s__subclass(s__NegativeRealNumber,s__RealNumber)),
% 12.66/4.16 file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_849)).
% 12.66/4.16 fof(f3410,axiom,(
% 12.66/4.16 ! [X0] : (s__instance(X0,s__RealNumber) => (s__instance(X0,s__NonnegativeRealNumber) => (s__SignumFn(X0) = "1" | s__SignumFn(X0) = "0")))),
% 12.66/4.16 file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_3422)).
% 12.66/4.16 fof(f3412,axiom,(
% 12.66/4.16 ! [X0] : (s__instance(X0,s__RealNumber) => (s__instance(X0,s__NegativeRealNumber) => s__SignumFn(X0) = "-1"))),
% 12.66/4.16 file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_3424)).
% 12.66/4.16 fof(f14788,axiom,(
% 12.66/4.16 s__instance(s__Number3_1,s__NonnegativeRealNumber)),
% 12.66/4.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_1)).
% 12.66/4.16 fof(f14789,conjecture,(
% 12.66/4.16 ~s__instance(s__Number3_1,s__NegativeRealNumber)),
% 12.66/4.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_SUMO)).
% 12.66/4.16 fof(f14790,negated_conjecture,(
% 12.66/4.16 ~ ~s__instance(s__Number3_1,s__NegativeRealNumber)),
% 12.66/4.16 inference(negated_conjecture,[status(cth)],[f14789])).
% 12.66/4.16 fof(f14791,plain,(
% 12.66/4.16 "1" != "2" & "1" != "3" & "2" != "3" & "1" != "-1" & "2" != "-1" & "3" != "-1" & "1" != "0" & "2" != "0" & "3" != "0" & "-1" != "0" & "1" != "4" & "2" != "4" & "3" != "4" & "-1" != "4" & "0" != "4" & "1" != "5" & "2" != "5" & "3" != "5" & "-1" != "5" & "0" != "5" & "4" != "5" & "1" != "0.5" & "2" != "0.5" & "3" != "0.5" & "-1" != "0.5" & "0" != "0.5" & "4" != "0.5" & "5" != "0.5" & "1" != "1000" & "2" != "1000" & "3" != "1000" & "-1" != "1000" & "0" != "1000" & "4" != "1000" & "5" != "1000" & "0.5" != "1000" & "1" != "1000000" & "2" != "1000000" & "3" != "1000000" & "-1" != "1000000" & "0" != "1000000" & "4" != "1000000" & "5" != "1000000" & "0.5" != "1000000" & "1000" != "1000000" & "1" != "1000000000" & "2" != "1000000000" & "3" != "1000000000" & "-1" != "1000000000" & "0" != "1000000000" & "4" != "1000000000" & "5" != "1000000000" & "0.5" != "1000000000" & "1000" != "1000000000" & "1000000" != "1000000000" & "1" != "1000000000000" & "2" != "1000000000000" & "3" != "1000000000000" & "-1" != "1000000000000" & "0" != "1000000000000" & "4" != "1000000000000" & "5" != "1000000000000" & "0.5" != "1000000000000" & "1000" != "1000000000000" & "1000000" != "1000000000000" & "1000000000" != "1000000000000" & "1" != "0.001" & "2" != "0.001" & "3" != "0.001" & "-1" != "0.001" & "0" != "0.001" & "4" != "0.001" & "5" != "0.001" & "0.5" != "0.001" & "1000" != "0.001" & "1000000" != "0.001" & "1000000000" != "0.001" & "1000000000000" != "0.001" & "1" != "0.000001" & "2" != "0.000001" & "3" != "0.000001" & "-1" != "0.000001" & "0" != "0.000001" & "4" != "0.000001" & "5" != "0.000001" & "0.5" != "0.000001" & "1000" != "0.000001" & "1000000" != "0.000001" & "1000000000" != "0.000001" & "1000000000000" != "0.000001" & "0.001" != "0.000001" & "1" != "0.000000001" & "2" != "0.000000001" & "3" != "0.000000001" & "-1" != "0.000000001" & "0" != "0.000000001" & "4" != "0.000000001" & "5" != "0.000000001" & "0.5" != "0.000000001" & "1000" != "0.000000001" & "1000000" != "0.000000001" & "1000000000" != "0.000000001" & "1000000000000" != "0.000000001" & "0.001" != "0.000000001" & "0.000001" != "0.000000001" & "1" != "0.000000000001" & "2" != "0.000000000001" & "3" != "0.000000000001" & "-1" != "0.000000000001" & "0" != "0.000000000001" & "4" != "0.000000000001" & "5" != "0.000000000001" & "0.5" != "0.000000000001" & "1000" != "0.000000000001" & "1000000" != "0.000000000001" & "1000000000" != "0.000000000001" & "1000000000000" != "0.000000000001" & "0.001" != "0.000000000001" & "0.000001" != "0.000000000001" & "0.000000001" != "0.000000000001" & "1" != "0.01" & "2" != "0.01" & "3" != "0.01" & "-1" != "0.01" & "0" != "0.01" & "4" != "0.01" & "5" != "0.01" & "0.5" != "0.01" & "1000" != "0.01" & "1000000" != "0.01" & "1000000000" != "0.01" & "1000000000000" != "0.01" & "0.001" != "0.01" & "0.000001" != "0.01" & "0.000000001" != "0.01" & "0.000000000001" != "0.01" & "1" != "746" & "2" != "746" & "3" != "746" & "-1" != "746" & "0" != "746" & "4" != "746" & "5" != "746" & "0.5" != "746" & "1000" != "746" & "1000000" != "746" & "1000000000" != "746" & "1000000000000" != "746" & "0.001" != "746" & "0.000001" != "746" & "0.000000001" != "746" & "0.000000000001" != "746" & "0.01" != "746" & "1" != "273.15" & "2" != "273.15" & "3" != "273.15" & "-1" != "273.15" & "0" != "273.15" & "4" != "273.15" & "5" != "273.15" & "0.5" != "273.15" & "1000" != "273.15" & "1000000" != "273.15" & "1000000000" != "273.15" & "1000000000000" != "273.15" & "0.001" != "273.15" & "0.000001" != "273.15" & "0.000000001" != "273.15" & "0.000000000001" != "273.15" & "0.01" != "273.15" & "746" != "273.15" & "1" != "32" & "2" != "32" & "3" != "32" & "-1" != "32" & "0" != "32" & "4" != "32" & "5" != "32" & "0.5" != "32" & "1000" != "32" & "1000000" != "32" & "1000000000" != "32" & "1000000000000" != "32" & "0.001" != "32" & "0.000001" != "32" & "0.000000001" != "32" & "0.000000000001" != "32" & "0.01" != "32" & "746" != "32" & "273.15" != "32" & "1" != "1.8" & "2" != "1.8" & "3" != "1.8" & "-1" != "1.8" & "0" != "1.8" & "4" != "1.8" & "5" != "1.8" & "0.5" != "1.8" & "1000" != "1.8" & "1000000" != "1.8" & "1000000000" != "1.8" & "1000000000000" != "1.8" & "0.001" != "1.8" & "0.000001" != "1.8" & "0.000000001" != "1.8" & "0.000000000001" != "1.8" & "0.01" != "1.8" & "746" != "1.8" & "273.15" != "1.8" & "32" != "1.8" & "1" != "24" & "2" != "24" & "3" != "24" & "-1" != "24" & "0" != "24" & "4" != "24" & "5" != "24" & "0.5" != "24" & "1000" != "24" & "1000000" != "24" & "1000000000" != "24" & "1000000000000" != "24" & "0.001" != "24" & "0.000001" != "24" & "0.000000001" != "24" & "0.000000000001" != "24" & "0.01" != "24" & "746" != "24" & "273.15" != "24" & "32" != "24" & "1.8" != "24" & "1" != "60" & "2" != "60" & "3" != "60" & "-1" != "60" & "0" != "60" & "4" != "60" & "5" != "60" & "0.5" != "60" & "1000" != "60" & "1000000" != "60" & "1000000000" != "60" & "1000000000000" != "60" & "0.001" != "60" & "0.000001" != "60" & "0.000000001" != "60" & "0.000000000001" != "60" & "0.01" != "60" & "746" != "60" & "273.15" != "60" & "32" != "60" & "1.8" != "60" & "24" != "60" & "1" != "7" & "2" != "7" & "3" != "7" & "-1" != "7" & "0" != "7" & "4" != "7" & "5" != "7" & "0.5" != "7" & "1000" != "7" & "1000000" != "7" & "1000000000" != "7" & "1000000000000" != "7" & "0.001" != "7" & "0.000001" != "7" & "0.000000001" != "7" & "0.000000000001" != "7" & "0.01" != "7" & "746" != "7" & "273.15" != "7" & "32" != "7" & "1.8" != "7" & "24" != "7" & "60" != "7" & "1" != "28" & "2" != "28" & "3" != "28" & "-1" != "28" & "0" != "28" & "4" != "28" & "5" != "28" & "0.5" != "28" & "1000" != "28" & "1000000" != "28" & "1000000000" != "28" & "1000000000000" != "28" & "0.001" != "28" & "0.000001" != "28" & "0.000000001" != "28" & "0.000000000001" != "28" & "0.01" != "28" & "746" != "28" & "273.15" != "28" & "32" != "28" & "1.8" != "28" & "24" != "28" & "60" != "28" & "7" != "28" & "1" != "31" & "2" != "31" & "3" != "31" & "-1" != "31" & "0" != "31" & "4" != "31" & "5" != "31" & "0.5" != "31" & "1000" != "31" & "1000000" != "31" & "1000000000" != "31" & "1000000000000" != "31" & "0.001" != "31" & "0.000001" != "31" & "0.000000001" != "31" & "0.000000000001" != "31" & "0.01" != "31" & "746" != "31" & "273.15" != "31" & "32" != "31" & "1.8" != "31" & "24" != "31" & "60" != "31" & "7" != "31" & "28" != "31" & "1" != "365" & "2" != "365" & "3" != "365" & "-1" != "365" & "0" != "365" & "4" != "365" & "5" != "365" & "0.5" != "365" & "1000" != "365" & "1000000" != "365" & "1000000000" != "365" & "1000000000000" != "365" & "0.001" != "365" & "0.000001" != "365" & "0.000000001" != "365" & "0.000000000001" != "365" & "0.01" != "365" & "746" != "365" & "273.15" != "365" & "32" != "365" & "1.8" != "365" & "24" != "365" & "60" != "365" & "7" != "365" & "28" != "365" & "31" != "365" & "1" != "1.6605402E-24" & "2" != "1.6605402E-24" & "3" != "1.6605402E-24" & "-1" != "1.6605402E-24" & "0" != "1.6605402E-24" & "4" != "1.6605402E-24" & "5" != "1.6605402E-24" & "0.5" != "1.6605402E-24" & "1000" != "1.6605402E-24" & "1000000" != "1.6605402E-24" & "1000000000" != "1.6605402E-24" & "1000000000000" != "1.6605402E-24" & "0.001" != "1.6605402E-24" & "0.000001" != "1.6605402E-24" & "0.000000001" != "1.6605402E-24" & "0.000000000001" != "1.6605402E-24" & "0.01" != "1.6605402E-24" & "746" != "1.6605402E-24" & "273.15" != "1.6605402E-24" & "32" != "1.6605402E-24" & "1.8" != "1.6605402E-24" & "24" != "1.6605402E-24" & "60" != "1.6605402E-24" & "7" != "1.6605402E-24" & "28" != "1.6605402E-24" & "31" != "1.6605402E-24" & "365" != "1.6605402E-24" & "1" != "1.60217733E-19" & "2" != "1.60217733E-19" & "3" != "1.60217733E-19" & "-1" != "1.60217733E-19" & "0" != "1.60217733E-19" & "4" != "1.60217733E-19" & "5" != "1.60217733E-19" & "0.5" != "1.60217733E-19" & "1000" != "1.60217733E-19" & "1000000" != "1.60217733E-19" & "1000000000" != "1.60217733E-19" & "1000000000000" != "1.60217733E-19" & "0.001" != "1.60217733E-19" & "0.000001" != "1.60217733E-19" & "0.000000001" != "1.60217733E-19" & "0.000000000001" != "1.60217733E-19" & "0.01" != "1.60217733E-19" & "746" != "1.60217733E-19" & "273.15" != "1.60217733E-19" & "32" != "1.60217733E-19" & "1.8" != "1.60217733E-19" & "24" != "1.60217733E-19" & "60" != "1.60217733E-19" & "7" != "1.60217733E-19" & "28" != "1.60217733E-19" & "31" != "1.60217733E-19" & "365" != "1.60217733E-19" & "1.6605402E-24" != "1.60217733E-19" & "1" != "1.0E-10" & "2" != "1.0E-10" & "3" != "1.0E-10" & "-1" != "1.0E-10" & "0" != "1.0E-10" & "4" != "1.0E-10" & "5" != "1.0E-10" & "0.5" != "1.0E-10" & "1000" != "1.0E-10" & "1000000" != "1.0E-10" & "1000000000" != "1.0E-10" & "1000000000000" != "1.0E-10" & "0.001" != "1.0E-10" & "0.000001" != "1.0E-10" & "0.000000001" != "1.0E-10" & "0.000000000001" != "1.0E-10" & "0.01" != "1.0E-10" & "746" != "1.0E-10" & "273.15" != "1.0E-10" & "32" != "1.0E-10" & "1.8" != "1.0E-10" & "24" != "1.0E-10" & "60" != "1.0E-10" & "7" != "1.0E-10" & "28" != "1.0E-10" & "31" != "1.0E-10" & "365" != "1.0E-10" & "1.6605402E-24" != "1.0E-10" & "1.60217733E-19" != "1.0E-10" & "1" != "0.3048" & "2" != "0.3048" & "3" != "0.3048" & "-1" != "0.3048" & "0" != "0.3048" & "4" != "0.3048" & "5" != "0.3048" & "0.5" != "0.3048" & "1000" != "0.3048" & "1000000" != "0.3048" & "1000000000" != "0.3048" & "1000000000000" != "0.3048" & "0.001" != "0.3048" & "0.000001" != "0.3048" & "0.000000001" != "0.3048" & "0.000000000001" != "0.3048" & "0.01" != "0.3048" & "746" != "0.3048" & "273.15" != "0.3048" & "32" != "0.3048" & "1.8" != "0.3048" & "24" != "0.3048" & "60" != "0.3048" & "7" != "0.3048" & "28" != "0.3048" & "31" != "0.3048" & "365" != "0.3048" & "1.6605402E-24" != "0.3048" & "1.60217733E-19" != "0.3048" & "1.0E-10" != "0.3048" & "1" != "0.0254" & "2" != "0.0254" & "3" != "0.0254" & "-1" != "0.0254" & "0" != "0.0254" & "4" != "0.0254" & "5" != "0.0254" & "0.5" != "0.0254" & "1000" != "0.0254" & "1000000" != "0.0254" & "1000000000" != "0.0254" & "1000000000000" != "0.0254" & "0.001" != "0.0254" & "0.000001" != "0.0254" & "0.000000001" != "0.0254" & "0.000000000001" != "0.0254" & "0.01" != "0.0254" & "746" != "0.0254" & "273.15" != "0.0254" & "32" != "0.0254" & "1.8" != "0.0254" & "24" != "0.0254" & "60" != "0.0254" & "7" != "0.0254" & "28" != "0.0254" & "31" != "0.0254" & "365" != "0.0254" & "1.6605402E-24" != "0.0254" & "1.60217733E-19" != "0.0254" & "1.0E-10" != "0.0254" & "0.3048" != "0.0254" & "1" != "1609.344" & "2" != "1609.344" & "3" != "1609.344" & "-1" != "1609.344" & "0" != "1609.344" & "4" != "1609.344" & "5" != "1609.344" & "0.5" != "1609.344" & "1000" != "1609.344" & "1000000" != "1609.344" & "1000000000" != "1609.344" & "1000000000000" != "1609.344" & "0.001" != "1609.344" & "0.000001" != "1609.344" & "0.000000001" != "1609.344" & "0.000000000001" != "1609.344" & "0.01" != "1609.344" & "746" != "1609.344" & "273.15" != "1609.344" & "32" != "1609.344" & "1.8" != "1609.344" & "24" != "1609.344" & "60" != "1609.344" & "7" != "1609.344" & "28" != "1609.344" & "31" != "1609.344" & "365" != "1609.344" & "1.6605402E-24" != "1609.344" & "1.60217733E-19" != "1609.344" & "1.0E-10" != "1609.344" & "0.3048" != "1609.344" & "0.0254" != "1609.344" & "1" != "3.785411784" & "2" != "3.785411784" & "3" != "3.785411784" & "-1" != "3.785411784" & "0" != "3.785411784" & "4" != "3.785411784" & "5" != "3.785411784" & "0.5" != "3.785411784" & "1000" != "3.785411784" & "1000000" != "3.785411784" & "1000000000" != "3.785411784" & "1000000000000" != "3.785411784" & "0.001" != "3.785411784" & "0.000001" != "3.785411784" & "0.000000001" != "3.785411784" & "0.000000000001" != "3.785411784" & "0.01" != "3.785411784" & "746" != "3.785411784" & "273.15" != "3.785411784" & "32" != "3.785411784" & "1.8" != "3.785411784" & "24" != "3.785411784" & "60" != "3.785411784" & "7" != "3.785411784" & "28" != "3.785411784" & "31" != "3.785411784" & "365" != "3.785411784" & "1.6605402E-24" != "3.785411784" & "1.60217733E-19" != "3.785411784" & "1.0E-10" != "3.785411784" & "0.3048" != "3.785411784" & "0.0254" != "3.785411784" & "1609.344" != "3.785411784" & "1" != "8" & "2" != "8" & "3" != "8" & "-1" != "8" & "0" != "8" & "4" != "8" & "5" != "8" & "0.5" != "8" & "1000" != "8" & "1000000" != "8" & "1000000000" != "8" & "1000000000000" != "8" & "0.001" != "8" & "0.000001" != "8" & "0.000000001" != "8" & "0.000000000001" != "8" & "0.01" != "8" & "746" != "8" & "273.15" != "8" & "32" != "8" & "1.8" != "8" & "24" != "8" & "60" != "8" & "7" != "8" & "28" != "8" & "31" != "8" & "365" != "8" & "1.6605402E-24" != "8" & "1.60217733E-19" != "8" & "1.0E-10" != "8" & "0.3048" != "8" & "0.0254" != "8" & "1609.344" != "8" & "3.785411784" != "8" & "1" != "4.54609" & "2" != "4.54609" & "3" != "4.54609" & "-1" != "4.54609" & "0" != "4.54609" & "4" != "4.54609" & "5" != "4.54609" & "0.5" != "4.54609" & "1000" != "4.54609" & "1000000" != "4.54609" & "1000000000" != "4.54609" & "1000000000000" != "4.54609" & "0.001" != "4.54609" & "0.000001" != "4.54609" & "0.000000001" != "4.54609" & "0.000000000001" != "4.54609" & "0.01" != "4.54609" & "746" != "4.54609" & "273.15" != "4.54609" & "32" != "4.54609" & "1.8" != "4.54609" & "24" != "4.54609" & "60" != "4.54609" & "7" != "4.54609" & "28" != "4.54609" & "31" != "4.54609" & "365" != "4.54609" & "1.6605402E-24" != "4.54609" & "1.60217733E-19" != "4.54609" & "1.0E-10" != "4.54609" & "0.3048" != "4.54609" & "0.0254" != "4.54609" & "1609.344" != "4.54609" & "3.785411784" != "4.54609" & "8" != "4.54609" & "1" != "453.59237" & "2" != "453.59237" & "3" != "453.59237" & "-1" != "453.59237" & "0" != "453.59237" & "4" != "453.59237" & "5" != "453.59237" & "0.5" != "453.59237" & "1000" != "453.59237" & "1000000" != "453.59237" & "1000000000" != "453.59237" & "1000000000000" != "453.59237" & "0.001" != "453.59237" & "0.000001" != "453.59237" & "0.000000001" != "453.59237" & "0.000000000001" != "453.59237" & "0.01" != "453.59237" & "746" != "453.59237" & "273.15" != "453.59237" & "32" != "453.59237" & "1.8" != "453.59237" & "24" != "453.59237" & "60" != "453.59237" & "7" != "453.59237" & "28" != "453.59237" & "31" != "453.59237" & "365" != "453.59237" & "1.6605402E-24" != "453.59237" & "1.60217733E-19" != "453.59237" & "1.0E-10" != "453.59237" & "0.3048" != "453.59237" & "0.0254" != "453.59237" & "1609.344" != "453.59237" & "3.785411784" != "453.59237" & "8" != "453.59237" & "4.54609" != "453.59237" & "1" != "14593.90" & "2" != "14593.90" & "3" != "14593.90" & "-1" != "14593.90" & "0" != "14593.90" & "4" != "14593.90" & "5" != "14593.90" & "0.5" != "14593.90" & "1000" != "14593.90" & "1000000" != "14593.90" & "1000000000" != "14593.90" & "1000000000000" != "14593.90" & "0.001" != "14593.90" & "0.000001" != "14593.90" & "0.000000001" != "14593.90" & "0.000000000001" != "14593.90" & "0.01" != "14593.90" & "746" != "14593.90" & "273.15" != "14593.90" & "32" != "14593.90" & "1.8" != "14593.90" & "24" != "14593.90" & "60" != "14593.90" & "7" != "14593.90" & "28" != "14593.90" & "31" != "14593.90" & "365" != "14593.90" & "1.6605402E-24" != "14593.90" & "1.60217733E-19" != "14593.90" & "1.0E-10" != "14593.90" & "0.3048" != "14593.90" & "0.0254" != "14593.90" & "1609.344" != "14593.90" & "3.785411784" != "14593.90" & "8" != "14593.90" & "4.54609" != "14593.90" & "453.59237" != "14593.90" & "1" != "4.448222" & "2" != "4.448222" & "3" != "4.448222" & "-1" != "4.448222" & "0" != "4.448222" & "4" != "4.448222" & "5" != "4.448222" & "0.5" != "4.448222" & "1000" != "4.448222" & "1000000" != "4.448222" & "1000000000" != "4.448222" & "1000000000000" != "4.448222" & "0.001" != "4.448222" & "0.000001" != "4.448222" & "0.000000001" != "4.448222" & "0.000000000001" != "4.448222" & "0.01" != "4.448222" & "746" != "4.448222" & "273.15" != "4.448222" & "32" != "4.448222" & "1.8" != "4.448222" & "24" != "4.448222" & "60" != "4.448222" & "7" != "4.448222" & "28" != "4.448222" & "31" != "4.448222" & "365" != "4.448222" & "1.6605402E-24" != "4.448222" & "1.60217733E-19" != "4.448222" & "1.0E-10" != "4.448222" & "0.3048" != "4.448222" & "0.0254" != "4.448222" & "1609.344" != "4.448222" & "3.785411784" != "4.448222" & "8" != "4.448222" & "4.54609" != "4.448222" & "453.59237" != "4.448222" & "14593.90" != "4.448222" & "1" != "4.1868" & "2" != "4.1868" & "3" != "4.1868" & "-1" != "4.1868" & "0" != "4.1868" & "4" != "4.1868" & "5" != "4.1868" & "0.5" != "4.1868" & "1000" != "4.1868" & "1000000" != "4.1868" & "1000000000" != "4.1868" & "1000000000000" != "4.1868" & "0.001" != "4.1868" & "0.000001" != "4.1868" & "0.000000001" != "4.1868" & "0.000000000001" != "4.1868" & "0.01" != "4.1868" & "746" != "4.1868" & "273.15" != "4.1868" & "32" != "4.1868" & "1.8" != "4.1868" & "24" != "4.1868" & "60" != "4.1868" & "7" != "4.1868" & "28" != "4.1868" & "31" != "4.1868" & "365" != "4.1868" & "1.6605402E-24" != "4.1868" & "1.60217733E-19" != "4.1868" & "1.0E-10" != "4.1868" & "0.3048" != "4.1868" & "0.0254" != "4.1868" & "1609.344" != "4.1868" & "3.785411784" != "4.1868" & "8" != "4.1868" & "4.54609" != "4.1868" & "453.59237" != "4.1868" & "14593.90" != "4.1868" & "4.448222" != "4.1868" & "1" != "1055.05585262" & "2" != "1055.05585262" & "3" != "1055.05585262" & "-1" != "1055.05585262" & "0" != "1055.05585262" & "4" != "1055.05585262" & "5" != "1055.05585262" & "0.5" != "1055.05585262" & "1000" != "1055.05585262" & "1000000" != "1055.05585262" & "1000000000" != "1055.05585262" & "1000000000000" != "1055.05585262" & "0.001" != "1055.05585262" & "0.000001" != "1055.05585262" & "0.000000001" != "1055.05585262" & "0.000000000001" != "1055.05585262" & "0.01" != "1055.05585262" & "746" != "1055.05585262" & "273.15" != "1055.05585262" & "32" != "1055.05585262" & "1.8" != "1055.05585262" & "24" != "1055.05585262" & "60" != "1055.05585262" & "7" != "1055.05585262" & "28" != "1055.05585262" & "31" != "1055.05585262" & "365" != "1055.05585262" & "1.6605402E-24" != "1055.05585262" & "1.60217733E-19" != "1055.05585262" & "1.0E-10" != "1055.05585262" & "0.3048" != "1055.05585262" & "0.0254" != "1055.05585262" & "1609.344" != "1055.05585262" & "3.785411784" != "1055.05585262" & "8" != "1055.05585262" & "4.54609" != "1055.05585262" & "453.59237" != "1055.05585262" & "14593.90" != "1055.05585262" & "4.448222" != "1055.05585262" & "4.1868" != "1055.05585262" & "1" != "180" & "2" != "180" & "3" != "180" & "-1" != "180" & "0" != "180" & "4" != "180" & "5" != "180" & "0.5" != "180" & "1000" != "180" & "1000000" != "180" & "1000000000" != "180" & "1000000000000" != "180" & "0.001" != "180" & "0.000001" != "180" & "0.000000001" != "180" & "0.000000000001" != "180" & "0.01" != "180" & "746" != "180" & "273.15" != "180" & "32" != "180" & "1.8" != "180" & "24" != "180" & "60" != "180" & "7" != "180" & "28" != "180" & "31" != "180" & "365" != "180" & "1.6605402E-24" != "180" & "1.60217733E-19" != "180" & "1.0E-10" != "180" & "0.3048" != "180" & "0.0254" != "180" & "1609.344" != "180" & "3.785411784" != "180" & "8" != "180" & "4.54609" != "180" & "453.59237" != "180" & "14593.90" != "180" & "4.448222" != "180" & "4.1868" != "180" & "1055.05585262" != "180" & "1" != "360" & "2" != "360" & "3" != "360" & "-1" != "360" & "0" != "360" & "4" != "360" & "5" != "360" & "0.5" != "360" & "1000" != "360" & "1000000" != "360" & "1000000000" != "360" & "1000000000000" != "360" & "0.001" != "360" & "0.000001" != "360" & "0.000000001" != "360" & "0.000000000001" != "360" & "0.01" != "360" & "746" != "360" & "273.15" != "360" & "32" != "360" & "1.8" != "360" & "24" != "360" & "60" != "360" & "7" != "360" & "28" != "360" & "31" != "360" & "365" != "360" & "1.6605402E-24" != "360" & "1.60217733E-19" != "360" & "1.0E-10" != "360" & "0.3048" != "360" & "0.0254" != "360" & "1609.344" != "360" & "3.785411784" != "360" & "8" != "360" & "4.54609" != "360" & "453.59237" != "360" & "14593.90" != "360" & "4.448222" != "360" & "4.1868" != "360" & "1055.05585262" != "360" & "180" != "360" & "1" != "1024" & "2" != "1024" & "3" != "1024" & "-1" != "1024" & "0" != "1024" & "4" != "1024" & "5" != "1024" & "0.5" != "1024" & "1000" != "1024" & "1000000" != "1024" & "1000000000" != "1024" & "1000000000000" != "1024" & "0.001" != "1024" & "0.000001" != "1024" & "0.000000001" != "1024" & "0.000000000001" != "1024" & "0.01" != "1024" & "746" != "1024" & "273.15" != "1024" & "32" != "1024" & "1.8" != "1024" & "24" != "1024" & "60" != "1024" & "7" != "1024" & "28" != "1024" & "31" != "1024" & "365" != "1024" & "1.6605402E-24" != "1024" & "1.60217733E-19" != "1024" & "1.0E-10" != "1024" & "0.3048" != "1024" & "0.0254" != "1024" & "1609.344" != "1024" & "3.785411784" != "1024" & "8" != "1024" & "4.54609" != "1024" & "453.59237" != "1024" & "14593.90" != "1024" & "4.448222" != "1024" & "4.1868" != "1024" & "1055.05585262" != "1024" & "180" != "1024" & "360" != "1024" & "1" != "100" & "2" != "100" & "3" != "100" & "-1" != "100" & "0" != "100" & "4" != "100" & "5" != "100" & "0.5" != "100" & "1000" != "100" & "1000000" != "100" & "1000000000" != "100" & "1000000000000" != "100" & "0.001" != "100" & "0.000001" != "100" & "0.000000001" != "100" & "0.000000000001" != "100" & "0.01" != "100" & "746" != "100" & "273.15" != "100" & "32" != "100" & "1.8" != "100" & "24" != "100" & "60" != "100" & "7" != "100" & "28" != "100" & "31" != "100" & "365" != "100" & "1.6605402E-24" != "100" & "1.60217733E-19" != "100" & "1.0E-10" != "100" & "0.3048" != "100" & "0.0254" != "100" & "1609.344" != "100" & "3.785411784" != "100" & "8" != "100" & "4.54609" != "100" & "453.59237" != "100" & "14593.90" != "100" & "4.448222" != "100" & "4.1868" != "100" & "1055.05585262" != "100" & "180" != "100" & "360" != "100" & "1024" != "100" & "1" != "400" & "2" != "400" & "3" != "400" & "-1" != "400" & "0" != "400" & "4" != "400" & "5" != "400" & "0.5" != "400" & "1000" != "400" & "1000000" != "400" & "1000000000" != "400" & "1000000000000" != "400" & "0.001" != "400" & "0.000001" != "400" & "0.000000001" != "400" & "0.000000000001" != "400" & "0.01" != "400" & "746" != "400" & "273.15" != "400" & "32" != "400" & "1.8" != "400" & "24" != "400" & "60" != "400" & "7" != "400" & "28" != "400" & "31" != "400" & "365" != "400" & "1.6605402E-24" != "400" & "1.60217733E-19" != "400" & "1.0E-10" != "400" & "0.3048" != "400" & "0.0254" != "400" & "1609.344" != "400" & "3.785411784" != "400" & "8" != "400" & "4.54609" != "400" & "453.59237" != "400" & "14593.90" != "400" & "4.448222" != "400" & "4.1868" != "400" & "1055.05585262" != "400" & "180" != "400" & "360" != "400" & "1024" != "400" & "100" != "400" & "1" != "29" & "2" != "29" & "3" != "29" & "-1" != "29" & "0" != "29" & "4" != "29" & "5" != "29" & "0.5" != "29" & "1000" != "29" & "1000000" != "29" & "1000000000" != "29" & "1000000000000" != "29" & "0.001" != "29" & "0.000001" != "29" & "0.000000001" != "29" & "0.000000000001" != "29" & "0.01" != "29" & "746" != "29" & "273.15" != "29" & "32" != "29" & "1.8" != "29" & "24" != "29" & "60" != "29" & "7" != "29" & "28" != "29" & "31" != "29" & "365" != "29" & "1.6605402E-24" != "29" & "1.60217733E-19" != "29" & "1.0E-10" != "29" & "0.3048" != "29" & "0.0254" != "29" & "1609.344" != "29" & "3.785411784" != "29" & "8" != "29" & "4.54609" != "29" & "453.59237" != "29" & "14593.90" != "29" & "4.448222" != "29" & "4.1868" != "29" & "1055.05585262" != "29" & "180" != "29" & "360" != "29" & "1024" != "29" & "100" != "29" & "400" != "29" & "1" != "30" & "2" != "30" & "3" != "30" & "-1" != "30" & "0" != "30" & "4" != "30" & "5" != "30" & "0.5" != "30" & "1000" != "30" & "1000000" != "30" & "1000000000" != "30" & "1000000000000" != "30" & "0.001" != "30" & "0.000001" != "30" & "0.000000001" != "30" & "0.000000000001" != "30" & "0.01" != "30" & "746" != "30" & "273.15" != "30" & "32" != "30" & "1.8" != "30" & "24" != "30" & "60" != "30" & "7" != "30" & "28" != "30" & "31" != "30" & "365" != "30" & "1.6605402E-24" != "30" & "1.60217733E-19" != "30" & "1.0E-10" != "30" & "0.3048" != "30" & "0.0254" != "30" & "1609.344" != "30" & "3.785411784" != "30" & "8" != "30" & "4.54609" != "30" & "453.59237" != "30" & "14593.90" != "30" & "4.448222" != "30" & "4.1868" != "30" & "1055.05585262" != "30" & "180" != "30" & "360" != "30" & "1024" != "30" & "100" != "30" & "400" != "30" & "29" != "30" & "1" != "12" & "2" != "12" & "3" != "12" & "-1" != "12" & "0" != "12" & "4" != "12" & "5" != "12" & "0.5" != "12" & "1000" != "12" & "1000000" != "12" & "1000000000" != "12" & "1000000000000" != "12" & "0.001" != "12" & "0.000001" != "12" & "0.000000001" != "12" & "0.000000000001" != "12" & "0.01" != "12" & "746" != "12" & "273.15" != "12" & "32" != "12" & "1.8" != "12" & "24" != "12" & "60" != "12" & "7" != "12" & "28" != "12" & "31" != "12" & "365" != "12" & "1.6605402E-24" != "12" & "1.60217733E-19" != "12" & "1.0E-10" != "12" & "0.3048" != "12" & "0.0254" != "12" & "1609.344" != "12" & "3.785411784" != "12" & "8" != "12" & "4.54609" != "12" & "453.59237" != "12" & "14593.90" != "12" & "4.448222" != "12" & "4.1868" != "12" & "1055.05585262" != "12" & "180" != "12" & "360" != "12" & "1024" != "12" & "100" != "12" & "400" != "12" & "29" != "12" & "30" != "12" & "1" != "29.92" & "2" != "29.92" & "3" != "29.92" & "-1" != "29.92" & "0" != "29.92" & "4" != "29.92" & "5" != "29.92" & "0.5" != "29.92" & "1000" != "29.92" & "1000000" != "29.92" & "1000000000" != "29.92" & "1000000000000" != "29.92" & "0.001" != "29.92" & "0.000001" != "29.92" & "0.000000001" != "29.92" & "0.000000000001" != "29.92" & "0.01" != "29.92" & "746" != "29.92" & "273.15" != "29.92" & "32" != "29.92" & "1.8" != "29.92" & "24" != "29.92" & "60" != "29.92" & "7" != "29.92" & "28" != "29.92" & "31" != "29.92" & "365" != "29.92" & "1.6605402E-24" != "29.92" & "1.60217733E-19" != "29.92" & "1.0E-10" != "29.92" & "0.3048" != "29.92" & "0.0254" != "29.92" & "1609.344" != "29.92" & "3.785411784" != "29.92" & "8" != "29.92" & "4.54609" != "29.92" & "453.59237" != "29.92" & "14593.90" != "29.92" & "4.448222" != "29.92" & "4.1868" != "29.92" & "1055.05585262" != "29.92" & "180" != "29.92" & "360" != "29.92" & "1024" != "29.92" & "100" != "29.92" & "400" != "29.92" & "29" != "29.92" & "30" != "29.92" & "12" != "29.92" & "1" != "6" & "2" != "6" & "3" != "6" & "-1" != "6" & "0" != "6" & "4" != "6" & "5" != "6" & "0.5" != "6" & "1000" != "6" & "1000000" != "6" & "1000000000" != "6" & "1000000000000" != "6" & "0.001" != "6" & "0.000001" != "6" & "0.000000001" != "6" & "0.000000000001" != "6" & "0.01" != "6" & "746" != "6" & "273.15" != "6" & "32" != "6" & "1.8" != "6" & "24" != "6" & "60" != "6" & "7" != "6" & "28" != "6" & "31" != "6" & "365" != "6" & "1.6605402E-24" != "6" & "1.60217733E-19" != "6" & "1.0E-10" != "6" & "0.3048" != "6" & "0.0254" != "6" & "1609.344" != "6" & "3.785411784" != "6" & "8" != "6" & "4.54609" != "6" & "453.59237" != "6" & "14593.90" != "6" & "4.448222" != "6" & "4.1868" != "6" & "1055.05585262" != "6" & "180" != "6" & "360" != "6" & "1024" != "6" & "100" != "6" & "400" != "6" & "29" != "6" & "30" != "6" & "12" != "6" & "29.92" != "6"),
% 12.66/4.16 introduced(theory,[distinctness_axiom])).
% 12.66/4.16 fof(f14794,plain,(
% 12.66/4.16 s__instance(s__Number3_1,s__NegativeRealNumber)),
% 12.66/4.16 inference(flattening,[],[f14790])).
% 12.66/4.16 fof(f14885,plain,(
% 12.66/4.16 ! [X0,X1] : ((s__instance(X0,s__SetOrClass) & s__instance(X1,s__SetOrClass)) | ~s__subclass(X0,X1))),
% 12.66/4.16 inference(ennf_transformation,[],[f26])).
% 12.66/4.16 fof(f14886,plain,(
% 12.66/4.16 ! [X0,X1,X2] : ((s__instance(X2,X1) | (~s__subclass(X0,X1) | ~s__instance(X2,X0))) | (~s__instance(X1,s__SetOrClass) | ~s__instance(X0,s__SetOrClass)))),
% 12.66/4.16 inference(ennf_transformation,[],[f27])).
% 12.66/4.16 fof(f14887,plain,(
% 12.66/4.16 ! [X0,X1,X2] : (s__instance(X2,X1) | ~s__subclass(X0,X1) | ~s__instance(X2,X0) | ~s__instance(X1,s__SetOrClass) | ~s__instance(X0,s__SetOrClass))),
% 12.66/4.16 inference(flattening,[],[f14886])).
% 12.66/4.16 fof(f18718,plain,(
% 12.66/4.16 ! [X0] : (((s__SignumFn(X0) = "1" | s__SignumFn(X0) = "0") | ~s__instance(X0,s__NonnegativeRealNumber)) | ~s__instance(X0,s__RealNumber))),
% 12.66/4.16 inference(ennf_transformation,[],[f3410])).
% 12.66/4.16 fof(f18719,plain,(
% 12.66/4.16 ! [X0] : (s__SignumFn(X0) = "1" | s__SignumFn(X0) = "0" | ~s__instance(X0,s__NonnegativeRealNumber) | ~s__instance(X0,s__RealNumber))),
% 12.66/4.16 inference(flattening,[],[f18718])).
% 12.66/4.16 fof(f18722,plain,(
% 12.66/4.16 ! [X0] : ((s__SignumFn(X0) = "-1" | ~s__instance(X0,s__NegativeRealNumber)) | ~s__instance(X0,s__RealNumber))),
% 12.66/4.16 inference(ennf_transformation,[],[f3412])).
% 12.66/4.16 fof(f18723,plain,(
% 12.66/4.16 ! [X0] : (s__SignumFn(X0) = "-1" | ~s__instance(X0,s__NegativeRealNumber) | ~s__instance(X0,s__RealNumber))),
% 12.66/4.16 inference(flattening,[],[f18722])).
% 12.66/4.16 fof(f21865,plain,(
% 12.66/4.16 "-1" != "0"),
% 12.66/4.16 inference(cnf_transformation,[],[f14791])).
% 12.66/4.16 fof(f21871,plain,(
% 12.66/4.16 "1" != "-1"),
% 12.66/4.16 inference(cnf_transformation,[],[f14791])).
% 12.66/4.16 fof(f21904,plain,(
% 12.66/4.16 ( ! [X0,X1] : (~s__subclass(X0,X1) | s__instance(X1,s__SetOrClass)) )),
% 12.66/4.16 inference(cnf_transformation,[],[f14885])).
% 12.66/4.16 fof(f21905,plain,(
% 12.66/4.16 ( ! [X0,X1] : (~s__subclass(X0,X1) | s__instance(X0,s__SetOrClass)) )),
% 12.66/4.16 inference(cnf_transformation,[],[f14885])).
% 12.66/4.16 fof(f21906,plain,(
% 12.66/4.16 ( ! [X2,X0,X1] : (s__instance(X2,X1) | ~s__subclass(X0,X1) | ~s__instance(X2,X0) | ~s__instance(X1,s__SetOrClass) | ~s__instance(X0,s__SetOrClass)) )),
% 12.66/4.16 inference(cnf_transformation,[],[f14887])).
% 12.66/4.16 fof(f22800,plain,(
% 12.66/4.16 s__subclass(s__NegativeRealNumber,s__RealNumber)),
% 12.66/4.16 inference(cnf_transformation,[],[f846])).
% 12.66/4.16 fof(f25531,plain,(
% 12.66/4.16 ( ! [X0] : (~s__instance(X0,s__NonnegativeRealNumber) | "0" = s__SignumFn(X0) | "1" = s__SignumFn(X0) | ~s__instance(X0,s__RealNumber)) )),
% 12.66/4.16 inference(cnf_transformation,[],[f18719])).
% 12.66/4.16 fof(f25533,plain,(
% 12.66/4.16 ( ! [X0] : (~s__instance(X0,s__NegativeRealNumber) | "-1" = s__SignumFn(X0) | ~s__instance(X0,s__RealNumber)) )),
% 12.66/4.16 inference(cnf_transformation,[],[f18723])).
% 12.66/4.16 fof(f37696,plain,(
% 12.66/4.16 s__instance(s__Number3_1,s__NonnegativeRealNumber)),
% 12.66/4.16 inference(cnf_transformation,[],[f14788])).
% 12.66/4.16 fof(f37697,plain,(
% 12.66/4.16 s__instance(s__Number3_1,s__NegativeRealNumber)),
% 12.66/4.16 inference(cnf_transformation,[],[f14794])).
% 12.66/4.16 fof(f48381,definition,(
% 12.66/4.16 spl504_76 <=> s__instance(s__Number3_1,s__RealNumber)),
% 12.66/4.16 introduced(definition,[new_symbols(definition,[spl504_76])],[avatar_definition])).
% 12.66/4.16 fof(f55869,plain,(
% 12.66/4.16 "-1" = s__SignumFn(s__Number3_1) | ~s__instance(s__Number3_1,s__RealNumber)),
% 12.66/4.16 inference(resolution,[],[f25533,f37697])).
% 12.66/4.16 fof(f55873,definition,(
% 12.66/4.16 spl504_1606 <=> "-1" = s__SignumFn(s__Number3_1)),
% 12.66/4.16 introduced(definition,[new_symbols(definition,[spl504_1606])],[avatar_definition])).
% 12.66/4.16 fof(f55875,plain,(
% 12.66/4.16 "-1" = s__SignumFn(s__Number3_1) | ~spl504_1606),
% 12.66/4.16 inference(avatar_component_clause,[],[f55873])).
% 12.66/4.16 fof(f55876,plain,(
% 12.66/4.16 ~spl504_76 | spl504_1606),
% 12.66/4.16 inference(avatar_split_clause,[],[f55869,f55873,f48381])).
% 12.66/4.16 fof(f60977,plain,(
% 12.66/4.16 "0" = s__SignumFn(s__Number3_1) | "1" = s__SignumFn(s__Number3_1) | ~s__instance(s__Number3_1,s__RealNumber)),
% 12.66/4.16 inference(resolution,[],[f25531,f37696])).
% 12.66/4.16 fof(f60985,plain,(
% 12.66/4.16 "-1" = "0" | "1" = s__SignumFn(s__Number3_1) | ~s__instance(s__Number3_1,s__RealNumber) | ~spl504_1606),
% 12.66/4.16 inference(forward_demodulation,[],[f60977,f55875])).
% 12.66/4.16 fof(f60997,plain,(
% 12.66/4.16 "1" = s__SignumFn(s__Number3_1) | ~s__instance(s__Number3_1,s__RealNumber) | ~spl504_1606),
% 12.66/4.16 inference(forward_subsumption_resolution,[],[f60985,f21865])).
% 12.66/4.16 fof(f61016,plain,(
% 12.66/4.16 "1" = "-1" | ~s__instance(s__Number3_1,s__RealNumber) | ~spl504_1606),
% 12.66/4.16 inference(forward_demodulation,[],[f60997,f55875])).
% 12.66/4.16 fof(f61017,plain,(
% 12.66/4.16 ~s__instance(s__Number3_1,s__RealNumber) | ~spl504_1606),
% 12.66/4.16 inference(forward_subsumption_resolution,[],[f61016,f21871])).
% 12.66/4.16 fof(f61018,plain,(
% 12.66/4.16 ~spl504_76 | ~spl504_1606),
% 12.66/4.16 inference(avatar_split_clause,[],[f61017,f55873,f48381])).
% 12.66/4.16 fof(f62257,plain,(
% 12.66/4.16 ( ! [X2,X0,X1] : (s__instance(X2,X1) | ~s__subclass(X0,X1) | ~s__instance(X2,X0) | ~s__instance(X0,s__SetOrClass)) )),
% 12.66/4.16 inference(forward_subsumption_resolution,[],[f21906,f21904])).
% 12.66/4.16 fof(f62258,plain,(
% 12.66/4.16 ( ! [X2,X0,X1] : (~s__instance(X2,X0) | ~s__subclass(X0,X1) | s__instance(X2,X1)) )),
% 12.66/4.16 inference(forward_subsumption_resolution,[],[f62257,f21905])).
% 12.66/4.16 fof(f66711,plain,(
% 12.66/4.16 ( ! [X0] : (~s__subclass(s__NegativeRealNumber,X0) | s__instance(s__Number3_1,X0)) )),
% 12.66/4.16 inference(resolution,[],[f62258,f37697])).
% 12.66/4.16 fof(f67162,plain,(
% 12.66/4.16 s__instance(s__Number3_1,s__RealNumber)),
% 12.66/4.16 inference(resolution,[],[f66711,f22800])).
% 12.66/4.16 fof(f67165,plain,(
% 12.66/4.16 spl504_76),
% 12.66/4.16 inference(avatar_split_clause,[],[f67162,f48381])).
% 12.66/4.16 cnf(s923, plain, ~spl504_76 | spl504_1606, inference(sat_conversion,[],[f55876])).
% 12.66/4.16 cnf(s1134, plain, ~spl504_76 | ~spl504_1606, inference(sat_conversion,[],[f61018])).
% 12.66/4.16 cnf(s1235, plain, spl504_76, inference(sat_conversion,[],[f67165])).
% 12.66/4.16 cnf(s1240, plain, ~spl504_1606, inference(rat,[],[s1134,s1235])).
% 12.66/4.16 cnf(s1264, plain, $false, inference(rat,[],[s923,s1240,s1235])).
% 12.66/4.16 fof(f67167,plain,(
% 12.66/4.16 $false),
% 12.66/4.16 inference(avatar_sat_refutation,[],[s1264])).
% 12.66/4.16 % SZS output end Proof for theBenchmark
% 12.66/4.16 % (2106573)------------------------------
% 12.66/4.16 % (2106573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.66/4.16 % (2106573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.66/4.16 % (2106573)CaDiCaL version: 2.1.3
% 12.66/4.16 % (2106573)Termination reason: Refutation
% 12.66/4.16 % (2106573)Time elapsed: 0.925 s
% 12.66/4.16 % (2106573)Peak memory usage: 53 MB
% 12.66/4.16 % (2106573)Instructions burned: 1771 (million)
% 12.66/4.16 % (2106512)Success in time 3.931 s
% 12.66/4.16 % Vampire exiting
%------------------------------------------------------------------------------