%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR077+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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 33.19s 5.18s
% Output : Refutation 33.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR077+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.23 % Computer : n015.cluster.edu
% 0.10/0.23 % Model : x86_64 x86_64
% 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.23 % Memory : 8046.5625MB
% 0.10/0.23 % OS : Linux 6.8.0-71-generic
% 0.10/0.23 % CPULimit : 300
% 0.10/0.23 % WCLimit : 300
% 0.10/0.23 % DateTime : Mon Sep 28 22:30:32 UTC 2026
% 0.10/0.24 % CPUTime :
% 0.10/0.24 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.26/0.28 Running first-order model finding
% 0.26/0.28 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.45/2.89 % (3106028)Will run a generic schedule for satisfiability detection.
% 14.45/2.89 % (3106034)% WARNING: option uhcvi not known.
% 14.45/2.89 % (3106034)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=618326251:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 14.45/2.89 % (3106037)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1254266601:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 14.45/2.89 % (3106033)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1695981152_2997 on theBenchmark for (2997ds/0Mi)
% 14.45/2.89 % (3106036)dis+10_1_sil=32000:sp=arity:random_seed=2779060573:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 14.45/2.89 % (3106035)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2916606494:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 14.45/2.89 % (3106039)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=505033085:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 14.45/2.89 % (3106038)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4099705723:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 14.45/2.89 % (3106037)Instruction limit reached!
% 14.45/2.89 % (3106037)------------------------------
% 14.45/2.89 % (3106037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.45/2.89 % (3106037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.45/2.89 % (3106037)CaDiCaL version: 2.1.3
% 14.45/2.89 % (3106037)Termination reason: Instruction limit
% 14.45/2.89 % (3106037)Termination phase: Property scanning
% 14.45/2.89 % (3106037)Time elapsed: 0.113 s
% 14.45/2.89 % (3106037)Peak memory usage: 26 MB
% 14.45/2.89 % (3106037)Instructions burned: 116 (million)
% 14.45/2.89 % (3106036)Instruction limit reached!
% 14.45/2.89 % (3106036)------------------------------
% 14.45/2.89 % (3106036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.45/2.89 % (3106036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.45/2.89 % (3106036)CaDiCaL version: 2.1.3
% 14.45/2.89 % (3106036)Termination reason: Instruction limit
% 14.45/2.89 % (3106036)Termination phase: Property scanning
% 14.45/2.89 % (3106036)Time elapsed: 0.104 s
% 14.45/2.89 % (3106036)Peak memory usage: 24 MB
% 14.45/2.89 % (3106036)Instructions burned: 105 (million)
% 14.45/2.89 % (3106048)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4089332640:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 14.45/2.89 % (3106038)Instruction limit reached!
% 14.45/2.89 % (3106038)------------------------------
% 14.45/2.89 % (3106038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.45/2.89 % (3106038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.45/2.89 % (3106038)CaDiCaL version: 2.1.3
% 14.45/2.89 % (3106038)Termination reason: Instruction limit
% 14.45/2.89 % (3106038)Termination phase: Property scanning
% 14.45/2.89 % (3106038)Time elapsed: 0.137 s
% 14.45/2.89 % (3106038)Peak memory usage: 24 MB
% 14.45/2.89 % (3106038)Instructions burned: 132 (million)
% 14.45/2.89 % (3106047)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2036709602:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi)
% 14.45/2.89 % (3106039)Instruction limit reached!
% 14.45/2.89 % (3106039)------------------------------
% 14.45/2.89 % (3106039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.45/2.89 % (3106039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.45/2.89 % (3106039)CaDiCaL version: 2.1.3
% 14.45/2.89 % (3106039)Termination reason: Instruction limit
% 14.45/2.89 % (3106039)Termination phase: Property scanning
% 14.45/2.89 % (3106039)Time elapsed: 0.160 s
% 14.45/2.89 % (3106039)Peak memory usage: 24 MB
% 14.45/2.89 % (3106039)Instructions burned: 159 (million)
% 14.45/2.89 % (3106051)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=1335594491:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 14.45/2.89 % (3106052)ott-21_1_sil=16000:fs=off:random_seed=373500068:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 14.45/2.89 % (3106048)Instruction limit reached!
% 14.45/2.89 % (3106048)------------------------------
% 14.45/2.89 % (3106048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.45/2.89 % (3106048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.10/4.19 % (3106048)CaDiCaL version: 2.1.3
% 26.10/4.19 % (3106048)Termination reason: Instruction limit
% 26.10/4.19 % (3106048)Termination phase: Property scanning
% 26.10/4.19 % (3106048)Time elapsed: 0.122 s
% 26.10/4.19 % (3106048)Peak memory usage: 24 MB
% 26.10/4.19 % (3106048)Instructions burned: 131 (million)
% 26.10/4.19 % (3106055)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2441115160:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi)
% 26.10/4.19 % (3106052)Instruction limit reached!
% 26.10/4.19 % (3106052)------------------------------
% 26.10/4.19 % (3106052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.10/4.19 % (3106052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.10/4.19 % (3106052)CaDiCaL version: 2.1.3
% 26.10/4.19 % (3106052)Termination reason: Instruction limit
% 26.10/4.19 % (3106052)Termination phase: Property scanning
% 26.10/4.19 % (3106052)Time elapsed: 0.182 s
% 26.10/4.19 % (3106052)Peak memory usage: 25 MB
% 26.10/4.19 % (3106052)Instructions burned: 181 (million)
% 26.10/4.19 % (3106057)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2541013528:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi)
% 26.10/4.19 % (3106047)Instruction limit reached!
% 26.10/4.19 % (3106047)------------------------------
% 26.10/4.19 % (3106047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.10/4.19 % (3106047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.10/4.19 % (3106047)CaDiCaL version: 2.1.3
% 26.10/4.19 % (3106047)Termination reason: Instruction limit
% 26.10/4.19 % (3106047)Termination phase: Finite model building preprocessing
% 26.10/4.19 % (3106047)Time elapsed: 0.611 s
% 26.10/4.19 % (3106047)Peak memory usage: 36 MB
% 26.10/4.19 % (3106047)Instructions burned: 714 (million)
% 26.10/4.19 % (3106055)Instruction limit reached!
% 26.10/4.19 % (3106055)------------------------------
% 26.10/4.19 % (3106055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.10/4.19 % (3106055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.10/4.19 % (3106055)CaDiCaL version: 2.1.3
% 26.10/4.19 % (3106055)Termination reason: Instruction limit
% 26.10/4.19 % (3106055)Termination phase: Saturation
% 26.10/4.19 % (3106055)Time elapsed: 0.457 s
% 26.10/4.19 % (3106055)Peak memory usage: 30 MB
% 26.10/4.19 % (3106055)Instructions burned: 477 (million)
% 26.10/4.19 % (3106059)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=15662978:i=1179_2989 on theBenchmark for (2989ds/1179Mi)
% 26.10/4.19 % (3106060)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1060003458:i=889:ins=1_2989 on theBenchmark for (2989ds/889Mi)
% 26.10/4.19 % (3106051)Instruction limit reached!
% 26.10/4.19 % (3106051)------------------------------
% 26.10/4.19 % (3106051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.10/4.19 % (3106051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.10/4.19 % (3106051)CaDiCaL version: 2.1.3
% 26.10/4.19 % (3106051)Termination reason: Instruction limit
% 26.10/4.19 % (3106051)Termination phase: Saturation
% 26.10/4.19 % (3106051)Time elapsed: 0.623 s
% 26.10/4.19 % (3106051)Peak memory usage: 33 MB
% 26.10/4.19 % (3106051)Instructions burned: 684 (million)
% 26.10/4.19 % (3106063)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=2097357171:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2989 on theBenchmark for (2989ds/692Mi)
% 26.10/4.19 % (3106057)Instruction limit reached!
% 26.10/4.19 % (3106057)------------------------------
% 26.10/4.19 % (3106057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.10/4.19 % (3106057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.10/4.19 % (3106057)CaDiCaL version: 2.1.3
% 26.10/4.19 % (3106057)Termination reason: Instruction limit
% 26.10/4.19 % (3106057)Termination phase: Finite model building preprocessing
% 26.10/4.19 % (3106057)Time elapsed: 0.725 s
% 26.10/4.19 % (3106057)Peak memory usage: 39 MB
% 26.10/4.19 % (3106057)Instructions burned: 866 (million)
% 26.10/4.19 % (3106065)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1141073371:i=879:kws=inv_precedence:fsr=off_2986 on theBenchmark for (2986ds/879Mi)
% 26.10/4.19 % Detected minimum model sizes of [51]
% 26.10/4.19 % Detected maximum model sizes of [max]
% 26.10/4.19 % (3106033)Cannot represent all propositional literals internally
% 26.10/4.19 % (3106033)Refutation not found, incomplete strategy
% 26.10/4.19 % (3106033)------------------------------
% 33.19/5.17 % (3106033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.17 % (3106033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.17 % (3106033)CaDiCaL version: 2.1.3
% 33.19/5.17 % (3106033)Termination reason: Refutation not found, incomplete strategy
% 33.19/5.17 % (3106033)Time elapsed: 1.257 s
% 33.19/5.17 % (3106033)Peak memory usage: 48 MB
% 33.19/5.17 % (3106033)Instructions burned: 1461 (million)
% 33.19/5.17 % (3106033)------------------------------
% 33.19/5.17 % (3106033)------------------------------
% 33.19/5.17 % (3106067)fmb+10_1_sil=64000:random_seed=3478953454:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi)
% 33.19/5.17 % (3106063)Instruction limit reached!
% 33.19/5.17 % (3106063)------------------------------
% 33.19/5.17 % (3106063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.17 % (3106063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.17 % (3106063)CaDiCaL version: 2.1.3
% 33.19/5.17 % (3106063)Termination reason: Instruction limit
% 33.19/5.17 % (3106063)Termination phase: Saturation
% 33.19/5.17 % (3106063)Time elapsed: 0.647 s
% 33.19/5.17 % (3106063)Peak memory usage: 35 MB
% 33.19/5.17 % (3106063)Instructions burned: 692 (million)
% 33.19/5.17 % (3106069)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=529111214:i=9515:nm=5_2982 on theBenchmark for (2982ds/9515Mi)
% 33.19/5.17 % (3106060)Instruction limit reached!
% 33.19/5.17 % (3106060)------------------------------
% 33.19/5.17 % (3106060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.17 % (3106060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.17 % (3106060)CaDiCaL version: 2.1.3
% 33.19/5.17 % (3106060)Termination reason: Instruction limit
% 33.19/5.17 % (3106060)Termination phase: Finite model building preprocessing
% 33.19/5.17 % (3106060)Time elapsed: 0.776 s
% 33.19/5.17 % (3106060)Peak memory usage: 40 MB
% 33.19/5.17 % (3106060)Instructions burned: 890 (million)
% 33.19/5.17 % (3106071)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=633218651:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi)
% 33.19/5.17 % (3106059)Instruction limit reached!
% 33.19/5.17 % (3106059)------------------------------
% 33.19/5.17 % (3106059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.17 % (3106059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.17 % (3106059)CaDiCaL version: 2.1.3
% 33.19/5.17 % (3106059)Termination reason: Instruction limit
% 33.19/5.17 % (3106059)Termination phase: Saturation
% 33.19/5.17 % (3106059)Time elapsed: 1.014 s
% 33.19/5.17 % (3106059)Peak memory usage: 36 MB
% 33.19/5.17 % (3106059)Instructions burned: 1179 (million)
% 33.19/5.17 % (3106075)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=652086130:i=5131_2979 on theBenchmark for (2979ds/5131Mi)
% 33.19/5.17 % (3106065)Instruction limit reached!
% 33.19/5.17 % (3106065)------------------------------
% 33.19/5.17 % (3106065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.17 % (3106065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.17 % (3106065)CaDiCaL version: 2.1.3
% 33.19/5.17 % (3106065)Termination reason: Instruction limit
% 33.19/5.17 % (3106065)Termination phase: Saturation
% 33.19/5.17 % (3106065)Time elapsed: 0.734 s
% 33.19/5.17 % (3106065)Peak memory usage: 38 MB
% 33.19/5.17 % (3106065)Instructions burned: 879 (million)
% 33.19/5.17 % (3106077)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=338936348:i=1472:ins=7:fdi=8:gsp=on_2978 on theBenchmark for (2978ds/1472Mi)
% 33.19/5.17 % Detected minimum model sizes of [51]
% 33.19/5.17 % Detected maximum model sizes of [max]
% 33.19/5.17 % (3106067)Cannot represent all propositional literals internally
% 33.19/5.17 % (3106067)Refutation not found, incomplete strategy
% 33.19/5.17 % (3106067)------------------------------
% 33.19/5.17 % (3106067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.17 % (3106067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.17 % (3106067)CaDiCaL version: 2.1.3
% 33.19/5.17 % (3106067)Termination reason: Refutation not found, incomplete strategy
% 33.19/5.17 % (3106067)Time elapsed: 0.992 s
% 33.19/5.17 % (3106067)Peak memory usage: 43 MB
% 33.19/5.17 % (3106067)Instructions burned: 1181 (million)
% 33.19/5.17 % (3106067)------------------------------
% 33.19/5.17 % (3106067)------------------------------
% 33.19/5.17 % (3106079)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=940689103:i=6324_2974 on theBenchmark for (2974ds/6324Mi)
% 33.19/5.17 % (3106071)Instruction limit reached!
% 33.19/5.17 % (3106071)------------------------------
% 33.19/5.17 % (3106071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.17 % (3106071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.17 % (3106071)CaDiCaL version: 2.1.3
% 33.19/5.17 % (3106071)Termination reason: Instruction limit
% 33.19/5.17 % (3106071)Termination phase: Finite model building preprocessing
% 33.19/5.17 % (3106071)Time elapsed: 0.779 s
% 33.19/5.17 % (3106071)Peak memory usage: 39 MB
% 33.19/5.17 % (3106071)Instructions burned: 920 (million)
% 33.19/5.17 % (3106081)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3764500637:fmbsr=2.30978:i=2174_2973 on theBenchmark for (2973ds/2174Mi)
% 33.19/5.17 % Detected minimum model sizes of [51]
% 33.19/5.17 % Detected maximum model sizes of [max]
% 33.19/5.17 % (3106069)Cannot represent all propositional literals internally
% 33.19/5.17 % (3106069)Refutation not found, incomplete strategy
% 33.19/5.17 % (3106069)------------------------------
% 33.19/5.17 % (3106069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.17 % (3106069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.17 % (3106069)CaDiCaL version: 2.1.3
% 33.19/5.17 % (3106069)Termination reason: Refutation not found, incomplete strategy
% 33.19/5.17 % (3106069)Time elapsed: 1.082 s
% 33.19/5.17 % (3106069)Peak memory usage: 44 MB
% 33.19/5.17 % (3106069)Instructions burned: 1256 (million)
% 33.19/5.17 % (3106069)------------------------------
% 33.19/5.17 % (3106069)------------------------------
% 33.19/5.17 % (3106083)ott-2_1_sil=16000:newcnf=on:random_seed=285648829:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 33.19/5.17 % (3106077)Instruction limit reached!
% 33.19/5.17 % (3106077)------------------------------
% 33.19/5.17 % (3106077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.17 % (3106077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.17 % (3106077)CaDiCaL version: 2.1.3
% 33.19/5.17 % (3106077)Termination reason: Instruction limit
% 33.19/5.17 % (3106077)Termination phase: Saturation
% 33.19/5.17 % (3106077)Time elapsed: 1.261 s
% 33.19/5.17 % (3106077)Peak memory usage: 44 MB
% 33.19/5.17 % (3106077)Instructions burned: 1473 (million)
% 33.19/5.17 % (3106086)ott+10_1_sil=32000:tgt=ground:random_seed=2791452717:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 33.19/5.17 % (3106083)Instruction limit reached!
% 33.19/5.17 % (3106083)------------------------------
% 33.19/5.17 % (3106083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.17 % (3106083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.17 % (3106083)CaDiCaL version: 2.1.3
% 33.19/5.17 % (3106083)Termination reason: Instruction limit
% 33.19/5.17 % (3106083)Termination phase: Saturation
% 33.19/5.17 % (3106083)Time elapsed: 0.655 s
% 33.19/5.17 % (3106083)Peak memory usage: 34 MB
% 33.19/5.17 % (3106083)Instructions burned: 869 (million)
% 33.19/5.17 % (3106088)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1593105186:i=54282_2964 on theBenchmark for (2964ds/54282Mi)
% 33.19/5.17 % Detected minimum model sizes of [51]
% 33.19/5.17 % Detected maximum model sizes of [max]
% 33.19/5.17 % (3106079)Cannot represent all propositional literals internally
% 33.19/5.17 % (3106079)Refutation not found, incomplete strategy
% 33.19/5.17 % (3106079)------------------------------
% 33.19/5.17 % (3106079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.17 % (3106079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.17 % (3106079)CaDiCaL version: 2.1.3
% 33.19/5.17 % (3106079)Termination reason: Refutation not found, incomplete strategy
% 33.19/5.17 % (3106079)Time elapsed: 1.050 s
% 33.19/5.17 % (3106079)Peak memory usage: 48 MB
% 33.19/5.17 % (3106079)Instructions burned: 1456 (million)
% 33.19/5.17 % (3106079)------------------------------
% 33.19/5.17 % (3106079)------------------------------
% 33.19/5.17 % (3106090)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1817746579:i=3512:aac=none_2963 on theBenchmark for (2963ds/3512Mi)
% 33.19/5.17 % (3106081)Instruction limit reached!
% 33.19/5.17 % (3106081)------------------------------
% 33.19/5.17 % (3106081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.17 % (3106081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.18 % (3106081)CaDiCaL version: 2.1.3
% 33.19/5.18 % (3106081)Termination reason: Instruction limit
% 33.19/5.18 % (3106081)Termination phase: Finite model building preprocessing
% 33.19/5.18 % (3106081)Time elapsed: 1.232 s
% 33.19/5.18 % (3106081)Peak memory usage: 62 MB
% 33.19/5.18 % (3106081)Instructions burned: 2175 (million)
% 33.19/5.18 % (3106109)dis+21_1_sil=32000:sas=cadical:random_seed=2646594355:i=3773:amm=off_2960 on theBenchmark for (2960ds/3773Mi)
% 33.19/5.18 % Detected minimum model sizes of [51]
% 33.19/5.18 % Detected maximum model sizes of [max]
% 33.19/5.18 % (3106088)Cannot represent all propositional literals internally
% 33.19/5.18 % (3106088)Refutation not found, incomplete strategy
% 33.19/5.18 % (3106088)------------------------------
% 33.19/5.18 % (3106088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.18 % (3106088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.18 % (3106088)CaDiCaL version: 2.1.3
% 33.19/5.18 % (3106088)Termination reason: Refutation not found, incomplete strategy
% 33.19/5.18 % (3106088)Time elapsed: 0.704 s
% 33.19/5.18 % (3106088)Peak memory usage: 49 MB
% 33.19/5.18 % (3106088)Instructions burned: 1469 (million)
% 33.19/5.18 % (3106088)------------------------------
% 33.19/5.18 % (3106088)------------------------------
% 33.19/5.18 % (3106133)ott+11_1_sil=16000:gs=on:random_seed=533580151:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2956 on theBenchmark for (2956ds/2251Mi)
% 33.19/5.18 % (3106109) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3106028-3106109"...
% 33.19/5.18 % (3106109)...printing done.
% 33.19/5.18 % (3106109)Refutation found. Thanks to Tanya!
% 33.19/5.18 % SZS status Theorem for theBenchmark
% 33.19/5.18 % SZS output start Proof for theBenchmark
% 33.19/5.18 fof(f26,axiom,(
% 33.19/5.18 ! [X0,X1] : (s__subclass(X0,X1) => (s__instance(X0,s__SetOrClass) & s__instance(X1,s__SetOrClass)))),
% 33.19/5.18 file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_26)).
% 33.19/5.18 fof(f27,axiom,(
% 33.19/5.18 ! [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)))),
% 33.19/5.18 file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_27)).
% 33.19/5.18 fof(f846,axiom,(
% 33.19/5.18 s__subclass(s__NegativeRealNumber,s__RealNumber)),
% 33.19/5.18 file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_849)).
% 33.19/5.18 fof(f3410,axiom,(
% 33.19/5.18 ! [X0] : (s__instance(X0,s__RealNumber) => (s__instance(X0,s__NonnegativeRealNumber) => (s__SignumFn(X0) = "1" | s__SignumFn(X0) = "0")))),
% 33.19/5.18 file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_3422)).
% 33.19/5.18 fof(f3412,axiom,(
% 33.19/5.18 ! [X0] : (s__instance(X0,s__RealNumber) => (s__instance(X0,s__NegativeRealNumber) => s__SignumFn(X0) = "-1"))),
% 33.19/5.18 file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_3424)).
% 33.19/5.18 fof(f7218,axiom,(
% 33.19/5.18 s__instance(s__Number3_1,s__NonnegativeRealNumber)),
% 33.19/5.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1)).
% 33.19/5.18 fof(f7219,conjecture,(
% 33.19/5.18 ~s__instance(s__Number3_1,s__NegativeRealNumber)),
% 33.19/5.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO)).
% 33.19/5.18 fof(f7220,negated_conjecture,(
% 33.19/5.18 ~ ~s__instance(s__Number3_1,s__NegativeRealNumber)),
% 33.19/5.18 inference(negated_conjecture,[status(cth)],[f7219])).
% 33.19/5.18 fof(f7221,plain,(
% 33.19/5.18 "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"),
% 33.19/5.18 introduced(theory,[distinctness_axiom])).
% 33.19/5.18 fof(f7224,plain,(
% 33.19/5.18 s__instance(s__Number3_1,s__NegativeRealNumber)),
% 33.19/5.18 inference(flattening,[],[f7220])).
% 33.19/5.18 fof(f7315,plain,(
% 33.19/5.18 ! [X0,X1] : ((s__instance(X0,s__SetOrClass) & s__instance(X1,s__SetOrClass)) | ~s__subclass(X0,X1))),
% 33.19/5.18 inference(ennf_transformation,[],[f26])).
% 33.19/5.18 fof(f7316,plain,(
% 33.19/5.18 ! [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)))),
% 33.19/5.18 inference(ennf_transformation,[],[f27])).
% 33.19/5.18 fof(f7317,plain,(
% 33.19/5.18 ! [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))),
% 33.19/5.18 inference(flattening,[],[f7316])).
% 33.19/5.18 fof(f11148,plain,(
% 33.19/5.18 ! [X0] : (((s__SignumFn(X0) = "1" | s__SignumFn(X0) = "0") | ~s__instance(X0,s__NonnegativeRealNumber)) | ~s__instance(X0,s__RealNumber))),
% 33.19/5.18 inference(ennf_transformation,[],[f3410])).
% 33.19/5.18 fof(f11149,plain,(
% 33.19/5.18 ! [X0] : (s__SignumFn(X0) = "1" | s__SignumFn(X0) = "0" | ~s__instance(X0,s__NonnegativeRealNumber) | ~s__instance(X0,s__RealNumber))),
% 33.19/5.18 inference(flattening,[],[f11148])).
% 33.19/5.18 fof(f11152,plain,(
% 33.19/5.18 ! [X0] : ((s__SignumFn(X0) = "-1" | ~s__instance(X0,s__NegativeRealNumber)) | ~s__instance(X0,s__RealNumber))),
% 33.19/5.18 inference(ennf_transformation,[],[f3412])).
% 33.19/5.18 fof(f11153,plain,(
% 33.19/5.18 ! [X0] : (s__SignumFn(X0) = "-1" | ~s__instance(X0,s__NegativeRealNumber) | ~s__instance(X0,s__RealNumber))),
% 33.19/5.18 inference(flattening,[],[f11152])).
% 33.19/5.18 fof(f14295,plain,(
% 33.19/5.18 "-1" != "0"),
% 33.19/5.18 inference(cnf_transformation,[],[f7221])).
% 33.19/5.18 fof(f14301,plain,(
% 33.19/5.18 "1" != "-1"),
% 33.19/5.18 inference(cnf_transformation,[],[f7221])).
% 33.19/5.18 fof(f14334,plain,(
% 33.19/5.18 ( ! [X0,X1] : (~s__subclass(X0,X1) | s__instance(X1,s__SetOrClass)) )),
% 33.19/5.18 inference(cnf_transformation,[],[f7315])).
% 33.19/5.18 fof(f14335,plain,(
% 33.19/5.18 ( ! [X0,X1] : (~s__subclass(X0,X1) | s__instance(X0,s__SetOrClass)) )),
% 33.19/5.18 inference(cnf_transformation,[],[f7315])).
% 33.19/5.18 fof(f14336,plain,(
% 33.19/5.18 ( ! [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)) )),
% 33.19/5.18 inference(cnf_transformation,[],[f7317])).
% 33.19/5.18 fof(f15230,plain,(
% 33.19/5.18 s__subclass(s__NegativeRealNumber,s__RealNumber)),
% 33.19/5.18 inference(cnf_transformation,[],[f846])).
% 33.19/5.18 fof(f17961,plain,(
% 33.19/5.18 ( ! [X0] : (~s__instance(X0,s__NonnegativeRealNumber) | "0" = s__SignumFn(X0) | "1" = s__SignumFn(X0) | ~s__instance(X0,s__RealNumber)) )),
% 33.19/5.18 inference(cnf_transformation,[],[f11149])).
% 33.19/5.18 fof(f17963,plain,(
% 33.19/5.18 ( ! [X0] : (~s__instance(X0,s__NegativeRealNumber) | "-1" = s__SignumFn(X0) | ~s__instance(X0,s__RealNumber)) )),
% 33.19/5.18 inference(cnf_transformation,[],[f11153])).
% 33.19/5.18 fof(f22556,plain,(
% 33.19/5.18 s__instance(s__Number3_1,s__NonnegativeRealNumber)),
% 33.19/5.18 inference(cnf_transformation,[],[f7218])).
% 33.19/5.18 fof(f22557,plain,(
% 33.19/5.18 s__instance(s__Number3_1,s__NegativeRealNumber)),
% 33.19/5.18 inference(cnf_transformation,[],[f7224])).
% 33.19/5.18 fof(f25061,definition,(
% 33.19/5.18 spl504_74 <=> s__instance(s__Number3_1,s__RealNumber)),
% 33.19/5.18 introduced(definition,[new_symbols(definition,[spl504_74])],[avatar_definition])).
% 33.19/5.18 fof(f25062,plain,(
% 33.19/5.18 ~s__instance(s__Number3_1,s__RealNumber) | spl504_74),
% 33.19/5.18 inference(avatar_component_clause,[],[f25061])).
% 33.19/5.18 fof(f33214,plain,(
% 33.19/5.18 "-1" = s__SignumFn(s__Number3_1) | ~s__instance(s__Number3_1,s__RealNumber)),
% 33.19/5.18 inference(resolution,[],[f17963,f22557])).
% 33.19/5.18 fof(f33218,definition,(
% 33.19/5.18 spl504_1828 <=> "-1" = s__SignumFn(s__Number3_1)),
% 33.19/5.18 introduced(definition,[new_symbols(definition,[spl504_1828])],[avatar_definition])).
% 33.19/5.18 fof(f33220,plain,(
% 33.19/5.18 "-1" = s__SignumFn(s__Number3_1) | ~spl504_1828),
% 33.19/5.18 inference(avatar_component_clause,[],[f33218])).
% 33.19/5.18 fof(f33221,plain,(
% 33.19/5.18 ~spl504_74 | spl504_1828),
% 33.19/5.18 inference(avatar_split_clause,[],[f33214,f33218,f25061])).
% 33.19/5.18 fof(f40511,plain,(
% 33.19/5.18 "0" = s__SignumFn(s__Number3_1) | "1" = s__SignumFn(s__Number3_1) | ~s__instance(s__Number3_1,s__RealNumber)),
% 33.19/5.18 inference(resolution,[],[f17961,f22556])).
% 33.19/5.18 fof(f40519,plain,(
% 33.19/5.18 "-1" = "0" | "1" = s__SignumFn(s__Number3_1) | ~s__instance(s__Number3_1,s__RealNumber) | ~spl504_1828),
% 33.19/5.18 inference(forward_demodulation,[],[f40511,f33220])).
% 33.19/5.18 fof(f40529,plain,(
% 33.19/5.18 "1" = s__SignumFn(s__Number3_1) | ~s__instance(s__Number3_1,s__RealNumber) | ~spl504_1828),
% 33.19/5.18 inference(forward_subsumption_resolution,[],[f40519,f14295])).
% 33.19/5.18 fof(f40530,plain,(
% 33.19/5.18 "1" = "-1" | ~s__instance(s__Number3_1,s__RealNumber) | ~spl504_1828),
% 33.19/5.18 inference(forward_demodulation,[],[f40529,f33220])).
% 33.19/5.18 fof(f40531,plain,(
% 33.19/5.18 ~s__instance(s__Number3_1,s__RealNumber) | ~spl504_1828),
% 33.19/5.18 inference(forward_subsumption_resolution,[],[f40530,f14301])).
% 33.19/5.18 fof(f40532,plain,(
% 33.19/5.18 ~spl504_74 | ~spl504_1828),
% 33.19/5.18 inference(avatar_split_clause,[],[f40531,f33218,f25061])).
% 33.19/5.18 fof(f43533,plain,(
% 33.19/5.18 ( ! [X2,X0,X1] : (s__instance(X2,X1) | ~s__subclass(X0,X1) | ~s__instance(X2,X0) | ~s__instance(X0,s__SetOrClass)) )),
% 33.19/5.18 inference(forward_subsumption_resolution,[],[f14336,f14334])).
% 33.19/5.18 fof(f43534,plain,(
% 33.19/5.18 ( ! [X2,X0,X1] : (~s__instance(X2,X0) | ~s__subclass(X0,X1) | s__instance(X2,X1)) )),
% 33.19/5.18 inference(forward_subsumption_resolution,[],[f43533,f14335])).
% 33.19/5.18 fof(f45732,plain,(
% 33.19/5.18 ( ! [X0] : (~s__subclass(s__NegativeRealNumber,X0) | s__instance(s__Number3_1,X0)) )),
% 33.19/5.18 inference(resolution,[],[f43534,f22557])).
% 33.19/5.18 fof(f46179,plain,(
% 33.19/5.18 s__instance(s__Number3_1,s__RealNumber)),
% 33.19/5.18 inference(resolution,[],[f45732,f15230])).
% 33.19/5.18 fof(f46182,plain,(
% 33.19/5.18 $false | spl504_74),
% 33.19/5.18 inference(forward_subsumption_resolution,[],[f46179,f25062])).
% 33.19/5.18 fof(f46183,plain,(
% 33.19/5.18 spl504_74),
% 33.19/5.18 inference(avatar_contradiction_clause,[],[f46182])).
% 33.19/5.18 cnf(s924, plain, ~spl504_74 | spl504_1828, inference(sat_conversion,[],[f33221])).
% 33.19/5.18 cnf(s1441, plain, ~spl504_74 | ~spl504_1828, inference(sat_conversion,[],[f40532])).
% 33.19/5.18 cnf(s1598, plain, spl504_74, inference(sat_conversion,[],[f46183])).
% 33.19/5.18 cnf(s1600, plain, ~spl504_1828, inference(rat,[],[s1441,s1598])).
% 33.19/5.18 cnf(s1644, plain, $false, inference(rat,[],[s924,s1600,s1598])).
% 33.19/5.18 fof(f46184,plain,(
% 33.19/5.18 $false),
% 33.19/5.18 inference(avatar_sat_refutation,[],[s1644])).
% 33.19/5.18 % SZS output end Proof for theBenchmark
% 33.19/5.18 % (3106109)------------------------------
% 33.19/5.18 % (3106109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.19/5.18 % (3106109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.19/5.18 % (3106109)CaDiCaL version: 2.1.3
% 33.19/5.18 % (3106109)Termination reason: Refutation
% 33.19/5.18 % (3106109)Time elapsed: 0.919 s
% 33.19/5.18 % (3106109)Peak memory usage: 42 MB
% 33.19/5.18 % (3106109)Instructions burned: 1981 (million)
% 33.19/5.18 % (3106028)Success in time 4.881 s
% 33.19/5.18 % Vampire exiting
%------------------------------------------------------------------------------