%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : DAT239^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 07:49:05 AM UTC 2026
% Result : Theorem 2.87s 0.64s
% Output : Refutation 2.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : DAT239^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n011.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Sep 29 18:13:46 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 Running first-order model finding
% 0.08/0.20 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
% 2.87/0.64 % (461726)Will run a generic schedule for satisfiability detection.
% 2.87/0.64 % (461733)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=692022852:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.87/0.64 % (461732)% WARNING: option uhcvi not known.
% 2.87/0.64 % (461731)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2718661014_2999 on theBenchmark for (2999ds/0Mi)
% 2.87/0.64 % (461732)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3986258015:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.87/0.64 % (461734)dis+10_1_sil=32000:sp=arity:random_seed=2935411521:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.87/0.64 % (461735)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3578630037:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.87/0.64 % (461736)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3586482299:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.87/0.64 % (461737)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2762841386:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.87/0.64 % (461732)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.87/0.64 % (461735)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.87/0.64 % Exception at run slice level
% 2.87/0.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.87/0.64 % (461732)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.87/0.64 % (461745)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1891680435:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.87/0.64 % (461734)Instruction limit reached!
% 2.87/0.64 % (461734)------------------------------
% 2.87/0.64 % (461734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.64 % (461734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.64 % (461734)CaDiCaL version: 2.1.3
% 2.87/0.64 % (461734)Termination reason: Instruction limit
% 2.87/0.64 % (461734)Termination phase: Saturation
% 2.87/0.64 % (461734)Time elapsed: 0.046 s
% 2.87/0.64 % (461734)Peak memory usage: 12 MB
% 2.87/0.64 % (461734)Instructions burned: 103 (million)
% 2.87/0.64 % (461735)Instruction limit reached!
% 2.87/0.64 % (461735)------------------------------
% 2.87/0.64 % (461735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.64 % (461735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.64 % (461735)CaDiCaL version: 2.1.3
% 2.87/0.64 % (461735)Termination reason: Instruction limit
% 2.87/0.64 % (461735)Termination phase: Saturation
% 2.87/0.64 % (461735)Time elapsed: 0.052 s
% 2.87/0.64 % (461735)Peak memory usage: 13 MB
% 2.87/0.64 % (461735)Instructions burned: 118 (million)
% 2.87/0.64 % (461736)Instruction limit reached!
% 2.87/0.64 % (461736)------------------------------
% 2.87/0.64 % (461736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.64 % (461736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.64 % (461736)CaDiCaL version: 2.1.3
% 2.87/0.64 % (461736)Termination reason: Instruction limit
% 2.87/0.64 % (461736)Termination phase: Saturation
% 2.87/0.64 % (461736)Time elapsed: 0.059 s
% 2.87/0.64 % (461736)Peak memory usage: 13 MB
% 2.87/0.64 % (461736)Instructions burned: 131 (million)
% 2.87/0.64 % (461747)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=540206093:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.87/0.64 % Exception at run slice level
% 2.87/0.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.87/0.64 % (461737)Instruction limit reached!
% 2.87/0.64 % (461737)------------------------------
% 2.87/0.64 % (461737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.64 % (461737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.64 % (461737)CaDiCaL version: 2.1.3
% 2.87/0.64 % (461737)Termination reason: Instruction limit
% 2.87/0.64 % (461737)Termination phase: Saturation
% 2.87/0.64 % (461737)Time elapsed: 0.070 s
% 2.87/0.64 % (461737)Peak memory usage: 13 MB
% 2.87/0.64 % (461737)Instructions burned: 159 (million)
% 2.87/0.64 % (461748)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=2254291840:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.87/0.64 % (461749)ott-21_1_sil=16000:fs=off:random_seed=1898556311:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.87/0.64 % (461748)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.87/0.64 % (461751)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3048405180:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.87/0.64 % (461753)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1768992238:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 2.87/0.64 % (461748)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.87/0.64 % Exception at run slice level
% 2.87/0.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.87/0.64 % (461747)Instruction limit reached!
% 2.87/0.64 % (461747)------------------------------
% 2.87/0.64 % (461747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.64 % (461747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.64 % (461747)CaDiCaL version: 2.1.3
% 2.87/0.64 % (461747)Termination reason: Instruction limit
% 2.87/0.64 % (461747)Termination phase: Saturation
% 2.87/0.64 % (461747)Time elapsed: 0.061 s
% 2.87/0.64 % (461747)Peak memory usage: 13 MB
% 2.87/0.64 % (461747)Instructions burned: 132 (million)
% 2.87/0.64 % (461757)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4228062053:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 2.87/0.64 % (461758)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3171073900:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 2.87/0.64 % (461749)Instruction limit reached!
% 2.87/0.64 % (461749)------------------------------
% 2.87/0.64 % (461749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.64 % (461749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.64 % (461749)CaDiCaL version: 2.1.3
% 2.87/0.64 % (461749)Termination reason: Instruction limit
% 2.87/0.64 % (461749)Termination phase: Saturation
% 2.87/0.64 % (461749)Time elapsed: 0.077 s
% 2.87/0.64 % (461749)Peak memory usage: 13 MB
% 2.87/0.64 % (461749)Instructions burned: 182 (million)
% 2.87/0.64 % (461761)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=2351613762:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 2.87/0.64 % Exception at run slice level
% 2.87/0.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.87/0.64 % (461761)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.87/0.64 % (461763)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1770564083:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 2.87/0.64 % (461763)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.87/0.64 % (461748)Instruction limit reached!
% 2.87/0.64 % (461748)------------------------------
% 2.87/0.64 % (461748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.64 % (461748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.64 % (461748)CaDiCaL version: 2.1.3
% 2.87/0.64 % (461748)Termination reason: Instruction limit
% 2.87/0.64 % (461748)Termination phase: Saturation
% 2.87/0.64 % (461748)Time elapsed: 0.218 s
% 2.87/0.64 % (461748)Peak memory usage: 14 MB
% 2.87/0.64 % (461748)Instructions burned: 685 (million)
% 2.87/0.64 % (461765)fmb+10_1_sil=64000:random_seed=3354401774:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 2.87/0.64 % (461751)Instruction limit reached!
% 2.87/0.64 % (461751)------------------------------
% 2.87/0.64 % (461751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.64 % (461751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.64 % (461751)CaDiCaL version: 2.1.3
% 2.87/0.64 % (461751)Termination reason: Instruction limit
% 2.87/0.64 % (461751)Termination phase: Saturation
% 2.87/0.64 % (461751)Time elapsed: 0.240 s
% 2.87/0.64 % (461751)Peak memory usage: 14 MB
% 2.87/0.64 % (461751)Instructions burned: 477 (million)
% 2.87/0.64 % (461765)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 2.87/0.64 % Exception at run slice level
% 2.87/0.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.87/0.64 % (461767)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4172169074:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 2.87/0.64 % (461768)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=108831437:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 2.87/0.64 % Exception at run slice level
% 2.87/0.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.87/0.64 % Exception at run slice level
% 2.87/0.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.87/0.64 % (461757) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-461726-461757"...
% 2.87/0.64 % (461757)...printing done.
% 2.87/0.64 % (461757)Refutation found. Thanks to Tanya!
% 2.87/0.64 % SZS status Theorem for theBenchmark
% 2.87/0.64 % SZS output start Proof for theBenchmark
% 2.87/0.64 thf(type_def_5, type, num: $tType).
% 2.87/0.64 thf(type_def_6, type, nat: $tType).
% 2.87/0.64 thf(type_def_7, type, int: $tType).
% 2.87/0.64 thf(type_def_8, type, itself: $tType > $tType).
% 2.87/0.64 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 2.87/0.64 thf(func_def_0, type, one: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_1, type, zero: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_2, type, numeral: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_3, type, field: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_4, type, neg_numeral: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_5, type, group_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_6, type, monoid_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_7, type, preorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_8, type, zero_neq_one: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_9, type, semiring_char_0: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_10, type, zero_less_one: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_11, type, semiring_div: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_12, type, division_ring: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_13, type, semigroup_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_14, type, semidom_divide: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_15, type, linordered_idom: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_16, type, linordered_field: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_17, type, ab_semigroup_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_18, type, linordered_semidom: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_19, type, semiring_div_parity: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_20, type, cancel_semigroup_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_21, type, semiring_numeral_div: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_22, type, cancel1352612707id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_23, type, linord219039673up_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_24, type, ordere779506340up_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_25, type, linord1659791738miring: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_26, type, canoni770627133id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_27, type, ordere236663937imp_le: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_28, type, ordere516151231imp_le: !>[X0: $tType]:((itself @ X0 > $o))).
% 2.87/0.64 thf(func_def_29, type, one_one: !>[X0: $tType]:(X0)).
% 2.87/0.64 thf(func_def_30, type, plus_plus: !>[X0: $tType]:((X0 > X0 > X0))).
% 2.87/0.64 thf(func_def_31, type, zero_zero: !>[X0: $tType]:(X0)).
% 2.87/0.64 thf(func_def_32, type, neg_numeral_dbl: !>[X0: $tType]:((X0 > X0))).
% 2.87/0.64 thf(func_def_33, type, bit0: (num > num)).
% 2.87/0.64 thf(func_def_34, type, one2: num).
% 2.87/0.64 thf(func_def_35, type, numeral_numeral: !>[X0: $tType]:((num > X0))).
% 2.87/0.64 thf(func_def_36, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.87/0.64 thf(func_def_37, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.87/0.64 thf(func_def_38, type, type: !>[X0: $tType]:(itself @ X0)).
% 2.87/0.64 thf(func_def_39, type, divide_divide: !>[X0: $tType]:((X0 > X0 > X0))).
% 2.87/0.64 thf(func_def_40, type, na: nat).
% 2.87/0.64 thf(func_def_44, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.87/0.64 thf(func_def_45, type, vNOT: ($o > $o)).
% 2.87/0.64 thf(func_def_46, type, vOR: ($o > $o > $o)).
% 2.87/0.64 thf(func_def_47, type, vAND: ($o > $o > $o)).
% 2.87/0.64 thf(func_def_48, type, db1: !>[X0: $tType]:(X0)).
% 2.87/0.64 thf(func_def_49, type, db0: !>[X0: $tType]:(X0)).
% 2.87/0.64 thf(func_def_50, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 2.87/0.64 thf(func_def_51, type, vIMP: ($o > $o > $o)).
% 2.87/0.64 thf(func_def_52, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.87/0.64 thf(func_def_53, type, db2: !>[X0: $tType]:(X0)).
% 2.87/0.64 thf(func_def_54, type, sK0: ((nat > nat) > nat)).
% 2.87/0.64 thf(func_def_55, type, sK1: ((nat > nat) > nat)).
% 2.87/0.64 thf(func_def_56, type, sK2: (nat > (nat > $o) > nat)).
% 2.87/0.64 thf(func_def_57, type, sK3: !>[X0: $tType]:((X0 > X0))).
% 2.87/0.64 thf(func_def_58, type, sK4: !>[X0: $tType]:((X0 > X0))).
% 2.87/0.64 thf(func_def_59, type, sK5: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 2.87/0.64 thf(func_def_60, type, sK6: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 2.87/0.64 thf(func_def_61, type, sK7: ((nat > $o) > nat)).
% 2.87/0.64 thf(func_def_62, type, sK8: ((nat > $o) > nat)).
% 2.87/0.64 thf(func_def_63, type, sK9: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 2.87/0.64 thf(func_def_64, type, sK10: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 2.87/0.64 thf(func_def_65, type, sK11: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 2.87/0.64 thf(func_def_66, type, sK12: ((nat > $o) > nat)).
% 2.87/0.64 thf(func_def_67, type, sF13: nat).
% 2.87/0.64 thf(func_def_68, type, sF14: num).
% 2.87/0.64 thf(func_def_69, type, sF15: nat).
% 2.87/0.64 thf(func_def_70, type, sF16: nat).
% 2.87/0.64 thf(func_def_71, type, sF17: $o).
% 2.87/0.64 thf(f1,axiom,(
% 2.87/0.64 ~((na = one_one @ nat) | (na = zero_zero @ nat))),
% 2.87/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_ns)).
% 2.87/0.64 thf(f2,axiom,(
% 2.87/0.64 ~(ord_less_eq @ nat @ na @ one_one @ nat)),
% 2.87/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_False)).
% 2.87/0.64 thf(f54,axiom,(
% 2.87/0.64 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X1 @ X0) | (ord_less_eq @ nat @ X0 @ X1))),
% 2.87/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_nat__le__linear)).
% 2.87/0.64 thf(f64,axiom,(
% 2.87/0.64 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X0 @ X1) => ((X0 != X1) => (ord_less @ nat @ X0 @ X1)))),
% 2.87/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_le__neq__implies__less)).
% 2.87/0.64 thf(f149,axiom,(
% 2.87/0.64 ! [X0 : nat] : ((ord_less @ nat @ one_one @ nat @ X0) => (ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ X0 @ (numeral_numeral @ nat @ (bit0 @ one2)))))),
% 2.87/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_div__2__gt__zero)).
% 2.87/0.64 thf(f301,conjecture,(
% 2.87/0.64 (ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ na @ (numeral_numeral @ nat @ (bit0 @ one2))))),
% 2.87/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 2.87/0.64 thf(f302,negated_conjecture,(
% 2.87/0.64 ~(ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ na @ (numeral_numeral @ nat @ (bit0 @ one2))))),
% 2.87/0.64 inference(negated_conjecture,[status(cth)],[f301])).
% 2.87/0.64 thf(f303,plain,(
% 2.87/0.64 ~(ord_less_eq @ nat @ na @ one_one @ nat)),
% 2.87/0.64 inference(rectify,[],[f2])).
% 2.87/0.64 thf(f304,plain,(
% 2.87/0.64 ~ (((ord_less_eq @ nat @ na @ one_one @ nat)) = $true)),
% 2.87/0.64 inference(fool_elimination,[],[f303])).
% 2.87/0.64 thf(f402,plain,(
% 2.87/0.64 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X1 @ X0) | (ord_less_eq @ nat @ X0 @ X1))),
% 2.87/0.64 inference(rectify,[],[f54])).
% 2.87/0.64 thf(f403,plain,(
% 2.87/0.64 ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ X0)) = $true) | (((ord_less_eq @ nat @ X0 @ X1)) = $true))),
% 2.87/0.64 inference(fool_elimination,[],[f402])).
% 2.87/0.64 thf(f421,plain,(
% 2.87/0.64 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X0 @ X1) => ((X0 != X1) => (ord_less @ nat @ X0 @ X1)))),
% 2.87/0.64 inference(rectify,[],[f64])).
% 2.87/0.64 thf(f422,plain,(
% 2.87/0.64 ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ X1)) = $true) => ((X0 != X1) => (((ord_less @ nat @ X0 @ X1)) = $true)))),
% 2.87/0.64 inference(fool_elimination,[],[f421])).
% 2.87/0.64 thf(f586,plain,(
% 2.87/0.64 ! [X0 : nat] : ((ord_less @ nat @ one_one @ nat @ X0) => (ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ X0 @ (numeral_numeral @ nat @ (bit0 @ one2)))))),
% 2.87/0.64 inference(rectify,[],[f149])).
% 2.87/0.64 thf(f587,plain,(
% 2.87/0.64 ! [X0 : nat] : ((((ord_less @ nat @ one_one @ nat @ X0)) = $true) => (((ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ X0 @ (numeral_numeral @ nat @ (bit0 @ one2))))) = $true))),
% 2.87/0.64 inference(fool_elimination,[],[f586])).
% 2.87/0.64 thf(f871,plain,(
% 2.87/0.64 ~(ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ na @ (numeral_numeral @ nat @ (bit0 @ one2))))),
% 2.87/0.64 inference(rectify,[],[f302])).
% 2.87/0.64 thf(f872,plain,(
% 2.87/0.64 ~ (((ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ na @ (numeral_numeral @ nat @ (bit0 @ one2))))) = $true)),
% 2.87/0.64 inference(fool_elimination,[],[f871])).
% 2.87/0.64 thf(f873,plain,(
% 2.87/0.64 (((ord_less_eq @ nat @ na @ one_one @ nat)) != $true)),
% 2.87/0.64 inference(flattening,[],[f304])).
% 2.87/0.64 thf(f898,plain,(
% 2.87/0.64 (((ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ na @ (numeral_numeral @ nat @ (bit0 @ one2))))) != $true)),
% 2.87/0.64 inference(flattening,[],[f872])).
% 2.87/0.64 thf(f899,plain,(
% 2.87/0.64 (na != one_one @ nat) & (na != zero_zero @ nat)),
% 2.87/0.64 inference(ennf_transformation,[],[f1])).
% 2.87/0.64 thf(f955,plain,(
% 2.87/0.64 ! [X0 : nat,X1 : nat] : (((((ord_less @ nat @ X0 @ X1)) = $true) | (X0 = X1)) | (((ord_less_eq @ nat @ X0 @ X1)) != $true))),
% 2.87/0.64 inference(ennf_transformation,[],[f422])).
% 2.87/0.64 thf(f956,plain,(
% 2.87/0.64 ! [X0 : nat,X1 : nat] : ((((ord_less @ nat @ X0 @ X1)) = $true) | (X0 = X1) | (((ord_less_eq @ nat @ X0 @ X1)) != $true))),
% 2.87/0.64 inference(flattening,[],[f955])).
% 2.87/0.64 thf(f1057,plain,(
% 2.87/0.64 ! [X0 : nat] : ((((ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ X0 @ (numeral_numeral @ nat @ (bit0 @ one2))))) = $true) | (((ord_less @ nat @ one_one @ nat @ X0)) != $true))),
% 2.87/0.64 inference(ennf_transformation,[],[f587])).
% 2.87/0.64 thf(f1167,plain,(
% 2.87/0.64 (na != one_one @ nat)),
% 2.87/0.64 inference(cnf_transformation,[],[f899])).
% 2.87/0.64 thf(f1168,plain,(
% 2.87/0.64 (((ord_less_eq @ nat @ na @ one_one @ nat)) != $true)),
% 2.87/0.64 inference(cnf_transformation,[],[f873])).
% 2.87/0.64 thf(f1221,plain,(
% 2.87/0.64 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ X0)) = $true) | (((ord_less_eq @ nat @ X0 @ X1)) = $true)) )),
% 2.87/0.64 inference(cnf_transformation,[],[f403])).
% 2.87/0.64 thf(f1232,plain,(
% 2.87/0.64 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ X1)) != $true) | (X0 = X1) | (((ord_less @ nat @ X0 @ X1)) = $true)) )),
% 2.87/0.64 inference(cnf_transformation,[],[f956])).
% 2.87/0.64 thf(f1332,plain,(
% 2.87/0.64 ( ! [X0 : nat] : ((((ord_less @ nat @ one_one @ nat @ X0)) != $true) | (((ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ X0 @ (numeral_numeral @ nat @ (bit0 @ one2))))) = $true)) )),
% 2.87/0.64 inference(cnf_transformation,[],[f1057])).
% 2.87/0.64 thf(f1484,plain,(
% 2.87/0.64 (((ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ na @ (numeral_numeral @ nat @ (bit0 @ one2))))) != $true)),
% 2.87/0.64 inference(cnf_transformation,[],[f898])).
% 2.87/0.64 thf(f1496,definition,(
% 2.87/0.64 (sF13 = zero_zero @ nat)),
% 2.87/0.64 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 2.87/0.64 thf(f1497,plain,(
% 2.87/0.64 (zero_zero @ nat = sF13)),
% 2.87/0.64 inference(reorient_equations,[],[f1496])).
% 2.87/0.64 thf(f1498,definition,(
% 2.87/0.64 (sF14 = ((bit0 @ one2)))),
% 2.87/0.64 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 2.87/0.64 thf(f1499,plain,(
% 2.87/0.64 (((bit0 @ one2)) = sF14)),
% 2.87/0.64 inference(reorient_equations,[],[f1498])).
% 2.87/0.64 thf(f1500,definition,(
% 2.87/0.64 (sF15 = ((numeral_numeral @ nat @ sF14)))),
% 2.87/0.64 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 2.87/0.64 thf(f1501,plain,(
% 2.87/0.64 (((numeral_numeral @ nat @ sF14)) = sF15)),
% 2.87/0.64 inference(reorient_equations,[],[f1500])).
% 2.87/0.64 thf(f1502,definition,(
% 2.87/0.64 (sF16 = ((divide_divide @ nat @ na @ sF15)))),
% 2.87/0.64 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 2.87/0.64 thf(f1503,plain,(
% 2.87/0.64 (((divide_divide @ nat @ na @ sF15)) = sF16)),
% 2.87/0.64 inference(reorient_equations,[],[f1502])).
% 2.87/0.64 thf(f1504,definition,(
% 2.87/0.64 (sF17 = ((ord_less @ nat @ sF13 @ sF16)))),
% 2.87/0.64 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 2.87/0.64 thf(f1505,plain,(
% 2.87/0.64 (((ord_less @ nat @ sF13 @ sF16)) = sF17)),
% 2.87/0.64 inference(reorient_equations,[],[f1504])).
% 2.87/0.64 thf(f1506,plain,(
% 2.87/0.64 ($true != sF17)),
% 2.87/0.64 inference(definition_folding,[],[f1484,f1505,f1503,f1501,f1499,f1497])).
% 2.87/0.64 thf(f2053,plain,(
% 2.87/0.64 ($false = ((ord_less @ nat @ sF13 @ sF16))) | ($true = sF17)),
% 2.87/0.64 inference(iff_proxy_clausification,[],[f1505])).
% 2.87/0.64 thf(f2054,plain,(
% 2.87/0.64 ($false = ((ord_less @ nat @ sF13 @ sF16)))),
% 2.87/0.64 inference(forward_subsumption_resolution,[],[f2053,f1506])).
% 2.87/0.64 thf(f3206,plain,(
% 2.87/0.64 ($true != $true) | ($true = ((ord_less_eq @ nat @ one_one @ nat @ na)))),
% 2.87/0.64 inference(constrained_superposition,[],[f1168,f1221])).
% 2.87/0.64 thf(f3217,plain,(
% 2.87/0.64 ($true = ((ord_less_eq @ nat @ one_one @ nat @ na)))),
% 2.87/0.64 inference(trivial_inequality_removal,[],[f3206])).
% 2.87/0.64 thf(f3755,plain,(
% 2.87/0.64 ($true != $true) | (na = one_one @ nat) | ($true = ((ord_less @ nat @ one_one @ nat @ na)))),
% 2.87/0.64 inference(constrained_superposition,[],[f1232,f3217])).
% 2.87/0.64 thf(f3758,plain,(
% 2.87/0.64 (na = one_one @ nat) | ($true = ((ord_less @ nat @ one_one @ nat @ na)))),
% 2.87/0.64 inference(trivial_inequality_removal,[],[f3755])).
% 2.87/0.64 thf(f3766,plain,(
% 2.87/0.64 ($true = ((ord_less @ nat @ one_one @ nat @ na)))),
% 2.87/0.64 inference(forward_subsumption_resolution,[],[f3758,f1167])).
% 2.87/0.64 thf(f6700,plain,(
% 2.87/0.64 ($true != $true) | (((ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ na @ (numeral_numeral @ nat @ (bit0 @ one2))))) = $true)),
% 2.87/0.64 inference(constrained_superposition,[],[f1332,f3766])).
% 2.87/0.64 thf(f6704,plain,(
% 2.87/0.64 (((ord_less @ nat @ zero_zero @ nat @ (divide_divide @ nat @ na @ (numeral_numeral @ nat @ (bit0 @ one2))))) = $true)),
% 2.87/0.64 inference(trivial_inequality_removal,[],[f6700])).
% 2.87/0.64 thf(f6707,plain,(
% 2.87/0.64 ($true = ((ord_less @ nat @ sF13 @ (divide_divide @ nat @ na @ (numeral_numeral @ nat @ (bit0 @ one2))))))),
% 2.87/0.64 inference(forward_demodulation,[],[f6704,f1497])).
% 2.87/0.64 thf(f6710,plain,(
% 2.87/0.64 ($true = ((ord_less @ nat @ sF13 @ (divide_divide @ nat @ na @ (numeral_numeral @ nat @ sF14)))))),
% 2.87/0.64 inference(forward_demodulation,[],[f6707,f1499])).
% 2.87/0.64 thf(f6713,plain,(
% 2.87/0.64 ($true = ((ord_less @ nat @ sF13 @ (divide_divide @ nat @ na @ sF15))))),
% 2.87/0.64 inference(forward_demodulation,[],[f6710,f1501])).
% 2.87/0.64 thf(f6716,plain,(
% 2.87/0.64 ($true = ((ord_less @ nat @ sF13 @ sF16)))),
% 2.87/0.64 inference(forward_demodulation,[],[f6713,f1503])).
% 2.87/0.64 thf(f6717,plain,(
% 2.87/0.64 ($true = $false)),
% 2.87/0.64 inference(forward_demodulation,[],[f6716,f2054])).
% 2.87/0.64 thf(f6718,plain,(
% 2.87/0.64 $false),
% 2.87/0.64 inference(trivial_inequality_removal,[],[f6717])).
% 2.87/0.64 % SZS output end Proof for theBenchmark
% 2.87/0.64 % (461757)------------------------------
% 2.87/0.64 % (461757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.64 % (461757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.64 % (461757)CaDiCaL version: 2.1.3
% 2.87/0.64 % (461757)Termination reason: Refutation
% 2.87/0.64 % (461757)Time elapsed: 0.246 s
% 2.87/0.64 % (461757)Peak memory usage: 16 MB
% 2.87/0.64 % (461757)Instructions burned: 510 (million)
% 2.87/0.64 % (461726)Success in time 0.438 s
% 2.87/0.64 % Vampire exiting
%------------------------------------------------------------------------------