%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP026^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 08:08:01 AM UTC 2026
% Result : Theorem 1.10s 0.52s
% Output : Refutation 1.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP026^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n005.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 19:38:01 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.21/0.28 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.43 % (2113342)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.46/0.43 % (2113349)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3411548622:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.46/0.43 % (2113349)Instruction limit reached!
% 0.46/0.43 % (2113349)------------------------------
% 0.46/0.43 % (2113349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.46/0.43 % (2113349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.46/0.43 % (2113349)CaDiCaL version: 2.1.3
% 0.46/0.43 % (2113349)Termination reason: Instruction limit
% 0.46/0.43 % (2113349)Termination phase: shuffling
% 0.46/0.43 % (2113349)Time elapsed: 0.004 s
% 0.46/0.43 % (2113349)Peak memory usage: 10 MB
% 0.46/0.43 % (2113349)Instructions burned: 15 (million)
% 0.46/0.43 % (2113353)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.46/0.43 % (2113353)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.46/0.43 % (2113347)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=4024980727:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.46/0.43 % (2113350)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=189102940:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.46/0.43 % (2113351)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3047921628:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.46/0.43 % (2113352)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=870011076:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.46/0.43 % (2113348)lrs+10_16_si=on:nwc=1.5:random_seed=630917685:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.46/0.43 % (2113353)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=2264375469:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.46/0.43 % (2113355)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3524378066:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.46/0.43 % (2113355)Instruction limit reached!
% 0.46/0.43 % (2113355)------------------------------
% 0.46/0.43 % (2113355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.46/0.43 % (2113355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.46/0.43 % (2113355)CaDiCaL version: 2.1.3
% 0.46/0.43 % (2113355)Termination reason: Instruction limit
% 0.46/0.43 % (2113355)Termination phase: shuffling
% 0.46/0.43 % (2113355)Time elapsed: 0.003 s
% 0.46/0.43 % (2113355)Peak memory usage: 10 MB
% 0.46/0.43 % (2113355)Instructions burned: 12 (million)
% 0.46/0.43 % (2113348)Instruction limit reached!
% 0.46/0.43 % (2113348)------------------------------
% 0.46/0.43 % (2113348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.46/0.43 % (2113348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.46/0.43 % (2113348)CaDiCaL version: 2.1.3
% 0.46/0.43 % (2113348)Termination reason: Instruction limit
% 0.46/0.43 % (2113348)Termination phase: shuffling
% 0.46/0.43 % (2113348)Time elapsed: 0.009 s
% 0.46/0.43 % (2113348)Peak memory usage: 10 MB
% 0.46/0.43 % (2113348)Instructions burned: 19 (million)
% 0.46/0.43 % (2113351)Instruction limit reached!
% 0.46/0.43 % (2113351)------------------------------
% 0.46/0.43 % (2113351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.46/0.43 % (2113351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.46/0.43 % (2113351)CaDiCaL version: 2.1.3
% 0.46/0.43 % (2113351)Termination reason: Instruction limit
% 0.46/0.43 % (2113351)Termination phase: shuffling
% 0.46/0.43 % (2113351)Time elapsed: 0.012 s
% 0.46/0.43 % (2113351)Peak memory usage: 10 MB
% 0.46/0.43 % (2113351)Instructions burned: 26 (million)
% 0.46/0.43 % (2113363)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1395229724:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.10/0.46 % (2113363)Instruction limit reached!
% 1.10/0.46 % (2113363)------------------------------
% 1.10/0.46 % (2113363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.46 % (2113363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.46 % (2113363)CaDiCaL version: 2.1.3
% 1.10/0.46 % (2113363)Termination reason: Instruction limit
% 1.10/0.46 % (2113363)Termination phase: shuffling
% 1.10/0.46 % (2113363)Time elapsed: 0.004 s
% 1.10/0.46 % (2113363)Peak memory usage: 10 MB
% 1.10/0.46 % (2113363)Instructions burned: 15 (million)
% 1.10/0.46 % (2113364)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.10/0.46 % (2113365)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=667659636:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.10/0.46 % (2113364)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1275193655:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.10/0.46 % (2113352)Instruction limit reached!
% 1.10/0.46 % (2113352)------------------------------
% 1.10/0.46 % (2113352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.46 % (2113352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.46 % (2113352)CaDiCaL version: 2.1.3
% 1.10/0.46 % (2113352)Termination reason: Instruction limit
% 1.10/0.46 % (2113352)Termination phase: Preprocessing 3
% 1.10/0.46 % (2113352)Time elapsed: 0.036 s
% 1.10/0.46 % (2113352)Peak memory usage: 11 MB
% 1.10/0.46 % (2113352)Instructions burned: 76 (million)
% 1.10/0.46 % (2113364)Instruction limit reached!
% 1.10/0.46 % (2113364)------------------------------
% 1.10/0.46 % (2113364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.46 % (2113364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.46 % (2113364)CaDiCaL version: 2.1.3
% 1.10/0.46 % (2113364)Termination reason: Instruction limit
% 1.10/0.46 % (2113364)Termination phase: shuffling
% 1.10/0.46 % (2113364)Time elapsed: 0.004 s
% 1.10/0.46 % (2113364)Peak memory usage: 10 MB
% 1.10/0.46 % (2113364)Instructions burned: 8 (million)
% 1.10/0.46 % (2113365)Instruction limit reached!
% 1.10/0.46 % (2113365)------------------------------
% 1.10/0.46 % (2113365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.46 % (2113365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.46 % (2113365)CaDiCaL version: 2.1.3
% 1.10/0.46 % (2113365)Termination reason: Instruction limit
% 1.10/0.46 % (2113365)Termination phase: shuffling
% 1.10/0.46 % (2113365)Time elapsed: 0.006 s
% 1.10/0.46 % (2113365)Peak memory usage: 10 MB
% 1.10/0.46 % (2113365)Instructions burned: 13 (million)
% 1.10/0.46 % (2113367)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.10/0.46 % (2113367)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.10/0.46 % (2113347)Instruction limit reached!
% 1.10/0.46 % (2113347)------------------------------
% 1.10/0.46 % (2113347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.46 % (2113347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.46 % (2113347)CaDiCaL version: 2.1.3
% 1.10/0.46 % (2113347)Termination reason: Instruction limit
% 1.10/0.46 % (2113347)Termination phase: Property scanning
% 1.10/0.46 % (2113347)Time elapsed: 0.042 s
% 1.10/0.46 % (2113347)Peak memory usage: 12 MB
% 1.10/0.46 % (2113347)Instructions burned: 89 (million)
% 1.10/0.46 % (2113367)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2371680062:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.10/0.46 % (2113372)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.10/0.46 % (2113372)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=2834613226:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.10/0.49 % (2113372)Instruction limit reached!
% 1.10/0.49 % (2113372)------------------------------
% 1.10/0.49 % (2113372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.49 % (2113372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.49 % (2113372)CaDiCaL version: 2.1.3
% 1.10/0.49 % (2113372)Termination reason: Instruction limit
% 1.10/0.49 % (2113372)Termination phase: shuffling
% 1.10/0.49 % (2113372)Time elapsed: 0.001 s
% 1.10/0.49 % (2113372)Peak memory usage: 10 MB
% 1.10/0.49 % (2113372)Instructions burned: 3 (million)
% 1.10/0.49 % (2113370)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=2120612588:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.10/0.49 % (2113371)lrs+10_1_si=on:cs=on:random_seed=3182239278:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.10/0.49 % (2113367)Instruction limit reached!
% 1.10/0.49 % (2113367)------------------------------
% 1.10/0.49 % (2113367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.49 % (2113367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.49 % (2113367)CaDiCaL version: 2.1.3
% 1.10/0.49 % (2113367)Termination reason: Instruction limit
% 1.10/0.49 % (2113367)Termination phase: shuffling
% 1.10/0.49 % (2113367)Time elapsed: 0.013 s
% 1.10/0.49 % (2113367)Peak memory usage: 10 MB
% 1.10/0.49 % (2113367)Instructions burned: 28 (million)
% 1.10/0.49 % (2113371)Instruction limit reached!
% 1.10/0.49 % (2113371)------------------------------
% 1.10/0.49 % (2113371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.49 % (2113371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.49 % (2113371)CaDiCaL version: 2.1.3
% 1.10/0.49 % (2113371)Termination reason: Instruction limit
% 1.10/0.49 % (2113371)Termination phase: shuffling
% 1.10/0.49 % (2113371)Time elapsed: 0.004 s
% 1.10/0.49 % (2113371)Peak memory usage: 10 MB
% 1.10/0.49 % (2113371)Instructions burned: 8 (million)
% 1.10/0.49 % (2113373)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2898991951:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 1.10/0.49 % (2113376)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2291322966:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.10/0.49 % (2113353)Instruction limit reached!
% 1.10/0.49 % (2113353)------------------------------
% 1.10/0.49 % (2113353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.49 % (2113353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.49 % (2113353)CaDiCaL version: 2.1.3
% 1.10/0.49 % (2113353)Termination reason: Instruction limit
% 1.10/0.49 % (2113353)Termination phase: Saturation
% 1.10/0.49 % (2113353)Time elapsed: 0.074 s
% 1.10/0.49 % (2113353)Peak memory usage: 13 MB
% 1.10/0.49 % (2113353)Instructions burned: 158 (million)
% 1.10/0.49 % (2113379)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=724897203:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.10/0.49 % (2113373)Instruction limit reached!
% 1.10/0.49 % (2113373)------------------------------
% 1.10/0.49 % (2113373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.49 % (2113373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.49 % (2113373)CaDiCaL version: 2.1.3
% 1.10/0.49 % (2113373)Termination reason: Instruction limit
% 1.10/0.49 % (2113373)Termination phase: Property scanning
% 1.10/0.49 % (2113373)Time elapsed: 0.017 s
% 1.10/0.49 % (2113373)Peak memory usage: 10 MB
% 1.10/0.49 % (2113373)Instructions burned: 38 (million)
% 1.10/0.49 % (2113380)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1780114435:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.10/0.49 % (2113380)Instruction limit reached!
% 1.10/0.49 % (2113380)------------------------------
% 1.10/0.49 % (2113380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.49 % (2113380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.49 % (2113380)CaDiCaL version: 2.1.3
% 1.10/0.49 % (2113380)Termination reason: Instruction limit
% 1.10/0.49 % (2113380)Termination phase: shuffling
% 1.10/0.49 % (2113380)Time elapsed: 0.007 s
% 1.10/0.52 % (2113380)Peak memory usage: 10 MB
% 1.10/0.52 % (2113380)Instructions burned: 16 (million)
% 1.10/0.52 % (2113379)Instruction limit reached!
% 1.10/0.52 % (2113379)------------------------------
% 1.10/0.52 % (2113379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113379)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113379)Termination reason: Instruction limit
% 1.10/0.52 % (2113379)Termination phase: shuffling
% 1.10/0.52 % (2113379)Time elapsed: 0.011 s
% 1.10/0.52 % (2113379)Peak memory usage: 10 MB
% 1.10/0.52 % (2113379)Instructions burned: 26 (million)
% 1.10/0.52 % (2113370)Instruction limit reached!
% 1.10/0.52 % (2113370)------------------------------
% 1.10/0.52 % (2113370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113370)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113370)Termination reason: Instruction limit
% 1.10/0.52 % (2113370)Termination phase: Property scanning
% 1.10/0.52 % (2113370)Time elapsed: 0.038 s
% 1.10/0.52 % (2113370)Peak memory usage: 11 MB
% 1.10/0.52 % (2113370)Instructions burned: 87 (million)
% 1.10/0.52 % (2113384)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3858185586:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.10/0.52 % (2113386)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3057315651:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.10/0.52 % (2113386)Instruction limit reached!
% 1.10/0.52 % (2113386)------------------------------
% 1.10/0.52 % (2113386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113386)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113386)Termination reason: Instruction limit
% 1.10/0.52 % (2113386)Termination phase: shuffling
% 1.10/0.52 % (2113386)Time elapsed: 0.007 s
% 1.10/0.52 % (2113386)Peak memory usage: 10 MB
% 1.10/0.52 % (2113386)Instructions burned: 15 (million)
% 1.10/0.52 % (2113387)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1148049210:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.10/0.52 % (2113388)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3038476819:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.10/0.52 % (2113387)Instruction limit reached!
% 1.10/0.52 % (2113387)------------------------------
% 1.10/0.52 % (2113387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113387)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113387)Termination reason: Instruction limit
% 1.10/0.52 % (2113387)Termination phase: shuffling
% 1.10/0.52 % (2113387)Time elapsed: 0.002 s
% 1.10/0.52 % (2113387)Peak memory usage: 10 MB
% 1.10/0.52 % (2113387)Instructions burned: 2 (million)
% 1.10/0.52 % (2113390)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1864270255:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.10/0.52 % (2113388)Instruction limit reached!
% 1.10/0.52 % (2113388)------------------------------
% 1.10/0.52 % (2113388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113388)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113388)Termination reason: Instruction limit
% 1.10/0.52 % (2113388)Termination phase: shuffling
% 1.10/0.52 % (2113388)Time elapsed: 0.013 s
% 1.10/0.52 % (2113388)Peak memory usage: 10 MB
% 1.10/0.52 % (2113388)Instructions burned: 28 (million)
% 1.10/0.52 % (2113395)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.10/0.52 % (2113395)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.10/0.52 % (2113392)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1681670755:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.10/0.52 % (2113390)Instruction limit reached!
% 1.10/0.52 % (2113390)------------------------------
% 1.10/0.52 % (2113390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113390)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113390)Termination reason: Instruction limit
% 1.10/0.52 % (2113390)Termination phase: shuffling
% 1.10/0.52 % (2113390)Time elapsed: 0.011 s
% 1.10/0.52 % (2113390)Peak memory usage: 10 MB
% 1.10/0.52 % (2113390)Instructions burned: 24 (million)
% 1.10/0.52 % (2113376)Instruction limit reached!
% 1.10/0.52 % (2113376)------------------------------
% 1.10/0.52 % (2113376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113376)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113376)Termination reason: Instruction limit
% 1.10/0.52 % (2113376)Termination phase: Saturation
% 1.10/0.52 % (2113376)Time elapsed: 0.064 s
% 1.10/0.52 % (2113376)Peak memory usage: 14 MB
% 1.10/0.52 % (2113376)Instructions burned: 249 (million)
% 1.10/0.52 % (2113395)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=383357301:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.10/0.52 % (2113395)Instruction limit reached!
% 1.10/0.52 % (2113395)------------------------------
% 1.10/0.52 % (2113395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113395)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113395)Termination reason: Instruction limit
% 1.10/0.52 % (2113395)Termination phase: shuffling
% 1.10/0.52 % (2113395)Time elapsed: 0.007 s
% 1.10/0.52 % (2113395)Peak memory usage: 10 MB
% 1.10/0.52 % (2113395)Instructions burned: 16 (million)
% 1.10/0.52 % (2113397)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.10/0.52 % (2113400)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=788434525:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.10/0.52 % (2113400)Instruction limit reached!
% 1.10/0.52 % (2113400)------------------------------
% 1.10/0.52 % (2113400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113400)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113400)Termination reason: Instruction limit
% 1.10/0.52 % (2113400)Termination phase: shuffling
% 1.10/0.52 % (2113400)Time elapsed: 0.002 s
% 1.10/0.52 % (2113400)Peak memory usage: 10 MB
% 1.10/0.52 % (2113400)Instructions burned: 8 (million)
% 1.10/0.52 % (2113397)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=1381977417:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.10/0.52 % (2113399)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=3944103348:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.10/0.52 % (2113397)Instruction limit reached!
% 1.10/0.52 % (2113397)------------------------------
% 1.10/0.52 % (2113397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113397)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113397)Termination reason: Instruction limit
% 1.10/0.52 % (2113397)Termination phase: shuffling
% 1.10/0.52 % (2113397)Time elapsed: 0.004 s
% 1.10/0.52 % (2113397)Peak memory usage: 10 MB
% 1.10/0.52 % (2113397)Instructions burned: 8 (million)
% 1.10/0.52 % (2113405)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3530912799:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.10/0.52 % (2113392)Instruction limit reached!
% 1.10/0.52 % (2113392)------------------------------
% 1.10/0.52 % (2113392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113392)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113392)Termination reason: Instruction limit
% 1.10/0.52 % (2113392)Termination phase: Preprocessing 3
% 1.10/0.52 % (2113392)Time elapsed: 0.028 s
% 1.10/0.52 % (2113392)Peak memory usage: 11 MB
% 1.10/0.52 % (2113392)Instructions burned: 62 (million)
% 1.10/0.52 % (2113402)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=151751919:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.10/0.52 % (2113405)Instruction limit reached!
% 1.10/0.52 % (2113405)------------------------------
% 1.10/0.52 % (2113405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113405)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113405)Termination reason: Instruction limit
% 1.10/0.52 % (2113405)Termination phase: shuffling
% 1.10/0.52 % (2113405)Time elapsed: 0.005 s
% 1.10/0.52 % (2113405)Peak memory usage: 10 MB
% 1.10/0.52 % (2113405)Instructions burned: 22 (million)
% 1.10/0.52 % (2113399)Instruction limit reached!
% 1.10/0.52 % (2113399)------------------------------
% 1.10/0.52 % (2113399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113399)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113399)Termination reason: Instruction limit
% 1.10/0.52 % (2113399)Termination phase: shuffling
% 1.10/0.52 % (2113399)Time elapsed: 0.015 s
% 1.10/0.52 % (2113399)Peak memory usage: 10 MB
% 1.10/0.52 % (2113399)Instructions burned: 33 (million)
% 1.10/0.52 % (2113407)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=166355760:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.10/0.52 % (2113402)Instruction limit reached!
% 1.10/0.52 % (2113402)------------------------------
% 1.10/0.52 % (2113402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113402)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113402)Termination reason: Instruction limit
% 1.10/0.52 % (2113402)Termination phase: shuffling
% 1.10/0.52 % (2113402)Time elapsed: 0.011 s
% 1.10/0.52 % (2113402)Peak memory usage: 10 MB
% 1.10/0.52 % (2113402)Instructions burned: 23 (million)
% 1.10/0.52 % (2113411)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1633968982:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 1.10/0.52 % (2113409)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2625404190:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 1.10/0.52 % (2113350) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2113342-2113350"...
% 1.10/0.52 % (2113412)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3808665588:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 1.10/0.52 % (2113350)...printing done.
% 1.10/0.52 % (2113350)Refutation found. Thanks to Tanya!
% 1.10/0.52 % SZS status Theorem for theBenchmark
% 1.10/0.52 % SZS output start Proof for theBenchmark
% 1.10/0.52 thf(type_def_5, type, carrier_ext: ($tType * $tType) > $tType).
% 1.10/0.52 thf(type_def_6, type, module_ext: ($tType * $tType * $tType) > $tType).
% 1.10/0.52 thf(type_def_7, type, aGroup_ext: ($tType * $tType) > $tType).
% 1.10/0.52 thf(type_def_8, type, ring_ext: ($tType * $tType) > $tType).
% 1.10/0.52 thf(type_def_9, type, product_unit: $tType).
% 1.10/0.52 thf(type_def_10, type, set: $tType > $tType).
% 1.10/0.52 thf(type_def_11, type, nat: $tType).
% 1.10/0.52 thf(type_def_12, type, f: $tType).
% 1.10/0.52 thf(type_def_13, type, e: $tType).
% 1.10/0.52 thf(type_def_14, type, d: $tType).
% 1.10/0.52 thf(type_def_15, type, c: $tType).
% 1.10/0.52 thf(type_def_16, type, b: $tType).
% 1.10/0.52 thf(type_def_17, type, a: $tType).
% 1.10/0.52 thf(type_def_18, type, sTfun: ($tType * $tType) > $tType).
% 1.10/0.52 thf(func_def_0, type, type: !>[X0: $tType]:($o)).
% 1.10/0.52 thf(func_def_1, type, zero: !>[X0: $tType]:($o)).
% 1.10/0.52 thf(func_def_2, type, order: !>[X0: $tType]:($o)).
% 1.10/0.52 thf(func_def_3, type, group_add: !>[X0: $tType]:($o)).
% 1.10/0.52 thf(func_def_4, type, wellorder: !>[X0: $tType]:($o)).
% 1.10/0.52 thf(func_def_5, type, comm_monoid_diff: !>[X0: $tType]:($o)).
% 1.10/0.52 thf(func_def_6, type, ordered_ab_group_add: !>[X0: $tType]:($o)).
% 1.10/0.52 thf(func_def_7, type, cancel1352612707id_add: !>[X0: $tType]:($o)).
% 1.10/0.52 thf(func_def_8, type, canoni770627133id_add: !>[X0: $tType]:($o)).
% 1.10/0.52 thf(func_def_9, type, carrier: !>[X0: $tType, X1: $tType]:((carrier_ext @ X0 @ X1 > set @ X0))).
% 1.10/0.52 thf(func_def_10, type, ring: !>[X0: $tType, X1: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > $o))).
% 1.10/0.52 thf(func_def_11, type, zero2: !>[X0: $tType, X1: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ X1 > X0))).
% 1.10/0.52 thf(func_def_12, type, ideal: !>[X0: $tType, X1: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > set @ X0 > $o))).
% 1.10/0.52 thf(func_def_13, type, annihilator: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > carrier_ext @ X2 @ aGroup_ext @ X2 @ module_ext @ X2 @ X0 @ X3 > set @ X0))).
% 1.10/0.52 thf(func_def_14, type, hom: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > carrier_ext @ X2 @ aGroup_ext @ X2 @ module_ext @ X2 @ X0 @ X3 > carrier_ext @ X4 @ aGroup_ext @ X4 @ module_ext @ X4 @ X0 @ X5 > carrier_ext @ (X2 > X4) @ aGroup_ext @ (X2 > X4) @ module_ext @ (X2 > X4) @ X0 @ product_unit))).
% 1.10/0.52 thf(func_def_15, type, module: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ module_ext @ X0 @ X1 @ X2 > carrier_ext @ X1 @ aGroup_ext @ X1 @ ring_ext @ X1 @ X3 > $o))).
% 1.10/0.52 thf(func_def_16, type, free_generator: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > carrier_ext @ X2 @ aGroup_ext @ X2 @ module_ext @ X2 @ X0 @ X3 > set @ X2 > $o))).
% 1.10/0.52 thf(func_def_17, type, generator: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > carrier_ext @ X2 @ aGroup_ext @ X2 @ module_ext @ X2 @ X0 @ X3 > set @ X2 > $o))).
% 1.10/0.52 thf(func_def_18, type, l_comb: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > carrier_ext @ X2 @ aGroup_ext @ X2 @ module_ext @ X2 @ X0 @ X3 > nat > (nat > X0) > (nat > X2) > X2))).
% 1.10/0.52 thf(func_def_19, type, linear_span: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > carrier_ext @ X2 @ aGroup_ext @ X2 @ module_ext @ X2 @ X0 @ X3 > set @ X0 > set @ X2 > set @ X2))).
% 1.10/0.52 thf(func_def_20, type, mdl: !>[X0: $tType, X1: $tType, X2: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ module_ext @ X0 @ X1 @ X2 > set @ X0 > carrier_ext @ X0 @ aGroup_ext @ X0 @ module_ext @ X0 @ X1 @ product_unit))).
% 1.10/0.52 thf(func_def_21, type, misomorphic: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > carrier_ext @ X2 @ aGroup_ext @ X2 @ module_ext @ X2 @ X0 @ X3 > carrier_ext @ X4 @ aGroup_ext @ X4 @ module_ext @ X4 @ X0 @ X5 > $o))).
% 1.10/0.52 thf(func_def_22, type, quotie135653060odules: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > carrier_ext @ X2 @ aGroup_ext @ X2 @ module_ext @ X2 @ X0 @ X3 > set @ X2 > set @ X2 > set @ X0))).
% 1.10/0.52 thf(func_def_23, type, smodule_ideal_coeff: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > carrier_ext @ X2 @ aGroup_ext @ X2 @ module_ext @ X2 @ X0 @ X3 > set @ X0 > set @ X2))).
% 1.10/0.52 thf(func_def_24, type, submodule: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > carrier_ext @ X2 @ aGroup_ext @ X2 @ module_ext @ X2 @ X0 @ X3 > set @ X2 > $o))).
% 1.10/0.52 thf(func_def_25, type, algebr833503410le_fgs: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((carrier_ext @ X0 @ aGroup_ext @ X0 @ ring_ext @ X0 @ X1 > carrier_ext @ X2 @ aGroup_ext @ X2 @ module_ext @ X2 @ X0 @ X3 > set @ X2 > set @ X2))).
% 1.10/0.52 thf(func_def_26, type, pi: !>[X0: $tType, X1: $tType]:((set @ X0 > (X0 > set @ X1) > set @ (X0 > X1)))).
% 1.10/0.52 thf(func_def_27, type, minus_minus: !>[X0: $tType]:((X0 > X0 > X0))).
% 1.10/0.52 thf(func_def_28, type, zero_zero: !>[X0: $tType]:(X0)).
% 1.10/0.52 thf(func_def_29, type, suc: (nat > nat)).
% 1.10/0.52 thf(func_def_30, type, bot_bot: !>[X0: $tType]:(X0)).
% 1.10/0.52 thf(func_def_31, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.10/0.52 thf(func_def_32, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.10/0.52 thf(func_def_33, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 1.10/0.52 thf(func_def_34, type, insert: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 1.10/0.52 thf(func_def_35, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 1.10/0.52 thf(func_def_36, type, h: set @ a).
% 1.10/0.52 thf(func_def_37, type, h1: set @ a).
% 1.10/0.52 thf(func_def_38, type, m: carrier_ext @ a @ aGroup_ext @ a @ module_ext @ a @ b @ c).
% 1.10/0.52 thf(func_def_39, type, n: carrier_ext @ e @ aGroup_ext @ e @ module_ext @ e @ b @ f).
% 1.10/0.52 thf(func_def_40, type, r: carrier_ext @ b @ aGroup_ext @ b @ ring_ext @ b @ d).
% 1.10/0.52 thf(func_def_41, type, g: (nat > a)).
% 1.10/0.52 thf(func_def_42, type, h2: a).
% 1.10/0.52 thf(func_def_43, type, m2: nat).
% 1.10/0.52 thf(func_def_44, type, t: (nat > b)).
% 1.10/0.52 thf(func_def_45, type, x: a).
% 1.10/0.52 thf(func_def_46, type, xa: nat).
% 1.10/0.52 thf(func_def_50, type, db0: !>[X0: $tType]:(X0)).
% 1.10/0.52 thf(func_def_51, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.10/0.52 thf(func_def_52, type, vAND: ($o > $o > $o)).
% 1.10/0.52 thf(func_def_53, type, db1: !>[X0: $tType]:(X0)).
% 1.10/0.52 thf(func_def_54, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.10/0.52 thf(func_def_55, type, vNOT: ($o > $o)).
% 1.10/0.52 thf(func_def_56, type, vOR: ($o > $o > $o)).
% 1.10/0.52 thf(func_def_57, type, sK0: ((nat > $o) > nat)).
% 1.10/0.52 thf(func_def_58, type, sK1: ((nat > $o) > nat > nat)).
% 1.10/0.52 thf(func_def_59, type, sK2: (set @ b > a > nat > b)).
% 1.10/0.52 thf(func_def_60, type, sK3: (set @ b > a > nat)).
% 1.10/0.52 thf(func_def_61, type, sK4: (set @ b > a > nat > a)).
% 1.10/0.52 thf(func_def_62, type, sK5: (nat > (nat > $o) > nat)).
% 1.10/0.52 thf(func_def_63, type, sK6: (nat > (nat > $o) > nat)).
% 1.10/0.52 thf(func_def_64, type, sK7: ((nat > $o) > nat)).
% 1.10/0.52 thf(func_def_65, type, sK8: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((set @ X0 > carrier_ext @ X1 @ aGroup_ext @ X1 @ ring_ext @ X1 @ X3 > carrier_ext @ X0 @ aGroup_ext @ X0 @ module_ext @ X0 @ X1 @ X2 > X0 > nat))).
% 1.10/0.52 thf(func_def_66, type, sK9: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((set @ X0 > carrier_ext @ X1 @ aGroup_ext @ X1 @ ring_ext @ X1 @ X3 > carrier_ext @ X0 @ aGroup_ext @ X0 @ module_ext @ X0 @ X1 @ X2 > X0 > nat > X0))).
% 1.10/0.52 thf(func_def_67, type, sK10: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((set @ X0 > carrier_ext @ X1 @ aGroup_ext @ X1 @ ring_ext @ X1 @ X3 > carrier_ext @ X0 @ aGroup_ext @ X0 @ module_ext @ X0 @ X1 @ X2 > X0 > nat > X1))).
% 1.10/0.52 thf(func_def_68, type, sK11: ((nat > $o) > nat)).
% 1.10/0.52 thf(func_def_69, type, sK12: !>[X0: $tType]:(((nat > X0) > nat))).
% 1.10/0.52 thf(func_def_70, type, sK13: ((nat > $o) > nat)).
% 1.10/0.52 thf(func_def_71, type, sK14: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_72, type, sK15: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_73, type, sK16: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_74, type, sK17: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_75, type, sK18: ((nat > $o) > nat > nat)).
% 1.10/0.52 thf(func_def_76, type, sK19: ((nat > nat) > nat)).
% 1.10/0.52 thf(func_def_77, type, sK20: ((nat > nat) > nat)).
% 1.10/0.52 thf(func_def_78, type, sK21: (nat > nat > nat)).
% 1.10/0.52 thf(func_def_79, type, sK22: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 1.10/0.52 thf(func_def_80, type, sK23: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 1.10/0.52 thf(func_def_81, type, sK24: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 1.10/0.52 thf(func_def_82, type, sK25: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > $o) > X0))).
% 1.10/0.52 thf(func_def_83, type, sK26: (set @ a > a > nat > a)).
% 1.10/0.52 thf(func_def_84, type, sK27: (set @ a > a > nat)).
% 1.10/0.52 thf(func_def_85, type, sK28: (set @ a > a > nat > b)).
% 1.10/0.52 thf(func_def_86, type, sK29: (nat > nat)).
% 1.10/0.52 thf(func_def_87, type, sK30: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((set @ X3 > carrier_ext @ X3 @ aGroup_ext @ X3 @ ring_ext @ X3 @ X2 > X0 > carrier_ext @ X0 @ aGroup_ext @ X0 @ module_ext @ X0 @ X3 @ X1 > nat))).
% 1.10/0.52 thf(func_def_88, type, sK31: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((set @ X3 > carrier_ext @ X3 @ aGroup_ext @ X3 @ ring_ext @ X3 @ X2 > X0 > carrier_ext @ X0 @ aGroup_ext @ X0 @ module_ext @ X0 @ X3 @ X1 > nat > X3))).
% 1.10/0.52 thf(func_def_89, type, sK32: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((set @ X3 > carrier_ext @ X3 @ aGroup_ext @ X3 @ ring_ext @ X3 @ X2 > X0 > carrier_ext @ X0 @ aGroup_ext @ X0 @ module_ext @ X0 @ X3 @ X1 > nat > X0))).
% 1.10/0.52 thf(func_def_90, type, sK33: ((nat > $o) > nat)).
% 1.10/0.52 thf(func_def_91, type, sK34: ((nat > $o) > nat)).
% 1.10/0.52 thf(func_def_92, type, sK35: (nat > (nat > $o) > nat)).
% 1.10/0.52 thf(func_def_93, type, sK36: (nat > (nat > $o) > nat)).
% 1.10/0.52 thf(func_def_94, type, sK37: (nat > (nat > $o) > nat)).
% 1.10/0.52 thf(func_def_95, type, sK38: ((nat > $o) > nat)).
% 1.10/0.52 thf(func_def_96, type, sK39: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_97, type, sK40: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_98, type, sK41: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_99, type, sK42: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_100, type, sK43: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_101, type, sK44: (nat > nat > nat)).
% 1.10/0.52 thf(func_def_102, type, sK45: !>[X0: $tType]:((set @ X0 > set @ X0 > X0))).
% 1.10/0.52 thf(func_def_103, type, sK46: (nat > (nat > $o) > nat)).
% 1.10/0.52 thf(func_def_104, type, sK47: (nat > (nat > $o) > nat)).
% 1.10/0.52 thf(func_def_105, type, sK48: (nat > nat)).
% 1.10/0.52 thf(func_def_106, type, sK49: (nat > nat)).
% 1.10/0.52 thf(func_def_107, type, sK50: !>[X0: $tType]:((set @ X0 > X0))).
% 1.10/0.52 thf(func_def_108, type, sK51: !>[X0: $tType]:((nat > (nat > X0) > (nat > X0) > nat))).
% 1.10/0.52 thf(func_def_109, type, sK52: ((nat > a) > (nat > a) > nat > nat)).
% 1.10/0.52 thf(func_def_110, type, sK53: ((nat > $o) > nat > nat > nat)).
% 1.10/0.52 thf(func_def_111, type, sK54: ((nat > $o) > nat)).
% 1.10/0.52 thf(func_def_112, type, sK55: ((nat > $o) > nat > nat)).
% 1.10/0.52 thf(func_def_113, type, sK56: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_114, type, sK57: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_115, type, sK58: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_116, type, sK59: ((nat > nat > $o) > nat)).
% 1.10/0.52 thf(func_def_117, type, sK60: !>[X0: $tType]:(((X0 > $o) > X0))).
% 1.10/0.52 thf(func_def_118, type, sK61: ((nat > $o) > nat)).
% 1.10/0.52 thf(func_def_119, type, sK62: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > $o) > X1))).
% 1.10/0.52 thf(func_def_120, type, sK63: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 1.10/0.52 thf(func_def_121, type, sK64: ((nat > $o) > nat > nat > nat)).
% 1.10/0.52 thf(func_def_122, type, sK65: ((nat > $o) > nat > nat)).
% 1.10/0.52 thf(func_def_123, type, sK66: ((nat > $o) > nat > nat)).
% 1.10/0.52 thf(func_def_124, type, sK67: !>[X0: $tType]:(((X0 > $o) > X0))).
% 1.10/0.52 thf(func_def_125, type, sK68: !>[X0: $tType]:(((nat > X0) > nat))).
% 1.10/0.52 thf(func_def_126, type, sK69: !>[X0: $tType]:(((nat > X0) > nat))).
% 1.10/0.52 thf(func_def_127, type, sK70: (nat > nat)).
% 1.10/0.52 thf(func_def_128, type, sK71: (nat > nat > nat)).
% 1.10/0.52 thf(func_def_129, type, sK72: !>[X0: $tType]:(((nat > X0) > nat))).
% 1.10/0.52 thf(func_def_130, type, sK73: (nat > nat)).
% 1.10/0.52 thf(func_def_131, type, sK74: ((nat > $o) > nat > nat)).
% 1.10/0.52 thf(func_def_132, type, sK75: ((nat > $o) > nat > nat)).
% 1.10/0.52 thf(func_def_133, type, sK76: !>[X0: $tType]:((nat > (nat > X0) > (nat > X0) > nat))).
% 1.10/0.52 thf(func_def_134, type, sK77: ((nat > a) > (nat > a) > nat > nat)).
% 1.10/0.52 thf(func_def_135, type, sK78: (nat > nat > nat)).
% 1.10/0.52 thf(func_def_137, type, inv_suc_80: (nat > nat)).
% 1.10/0.52 thf(f27,axiom,(
% 1.10/0.52 ! [X0 : nat] : ((ord_less @ nat @ zero_zero @ nat @ X0) => (((suc @ (minus_minus @ nat @ X0 @ (suc @ zero_zero @ nat)))) = X0))),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_Suc__pred)).
% 1.10/0.52 thf(f69,axiom,(
% 1.10/0.52 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X1 @ X0) | (ord_less_eq @ nat @ X0 @ X1))),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_nat__le__linear)).
% 1.10/0.52 thf(f70,axiom,(
% 1.10/0.52 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X0 @ X1) => ((ord_less_eq @ nat @ X1 @ X0) => (X0 = X1)))),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_le__antisym)).
% 1.10/0.52 thf(f71,axiom,(
% 1.10/0.52 ! [X0 : nat,X1 : nat,X2 : nat] : ((ord_less_eq @ nat @ X0 @ X1) => ((ord_less_eq @ nat @ X1 @ X2) => (ord_less_eq @ nat @ X0 @ X2)))),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_le__trans)).
% 1.10/0.52 thf(f72,axiom,(
% 1.10/0.52 ! [X0 : nat] : (X0 != ((suc @ X0)))),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_n__not__Suc__n)).
% 1.10/0.52 thf(f146,axiom,(
% 1.10/0.52 ! [X0 : nat,X1 : nat] : (ord_less_eq @ nat @ (minus_minus @ nat @ X0 @ X1) @ X0)),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_diff__le__self)).
% 1.10/0.52 thf(f152,axiom,(
% 1.10/0.52 ! [X0 : nat] : (((minus_minus @ nat @ X0 @ zero_zero @ nat)) = X0)),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_minus__nat_Odiff__0)).
% 1.10/0.52 thf(f266,axiom,(
% 1.10/0.52 ! [X0 : nat] : ((ord_less_eq @ nat @ X0 @ m2) => ! [X1 : nat] : ((ord_less_eq @ nat @ X1 @ m2) => ((((g @ X0)) = ((g @ X1))) => (X0 = X1))))),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1)).
% 1.10/0.52 thf(f268,axiom,(
% 1.10/0.52 (((g @ m2)) = h2)),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_3)).
% 1.10/0.52 thf(f281,axiom,(
% 1.10/0.52 (ord_less @ nat @ zero_zero @ nat @ m2)),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_16)).
% 1.10/0.52 thf(f284,axiom,(
% 1.10/0.52 (ord_less_eq @ nat @ xa @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)))),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_19)).
% 1.10/0.52 thf(f285,axiom,(
% 1.10/0.52 (member @ a @ (g @ xa) @ h1) | (((g @ xa)) = h2)),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_20)).
% 1.10/0.52 thf(f286,conjecture,(
% 1.10/0.52 (member @ a @ (g @ xa) @ h1)),
% 1.10/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_21)).
% 1.10/0.52 thf(f287,negated_conjecture,(
% 1.10/0.52 ~(member @ a @ (g @ xa) @ h1)),
% 1.10/0.52 inference(negated_conjecture,[status(cth)],[f286])).
% 1.10/0.52 thf(f296,plain,(
% 1.10/0.52 ! [X0 : nat,X1 : nat] : (ord_less_eq @ nat @ (minus_minus @ nat @ X0 @ X1) @ X0)),
% 1.10/0.52 inference(rectify,[],[f146])).
% 1.10/0.52 thf(f297,plain,(
% 1.10/0.52 ! [X1 : nat,X0 : nat] : (((ord_less_eq @ nat @ (minus_minus @ nat @ X0 @ X1) @ X0)) = $true)),
% 1.10/0.52 inference(fool_elimination,[],[f296])).
% 1.10/0.52 thf(f314,plain,(
% 1.10/0.52 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X0 @ X1) => ((ord_less_eq @ nat @ X1 @ X0) => (X0 = X1)))),
% 1.10/0.52 inference(rectify,[],[f70])).
% 1.10/0.52 thf(f315,plain,(
% 1.10/0.52 ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ X1)) = $true) => ((((ord_less_eq @ nat @ X1 @ X0)) = $true) => (X0 = X1)))),
% 1.10/0.52 inference(fool_elimination,[],[f314])).
% 1.10/0.52 thf(f322,plain,(
% 1.10/0.52 (ord_less_eq @ nat @ xa @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)))),
% 1.10/0.52 inference(rectify,[],[f284])).
% 1.10/0.52 thf(f323,plain,(
% 1.10/0.52 (((ord_less_eq @ nat @ xa @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)))) = $true)),
% 1.10/0.52 inference(fool_elimination,[],[f322])).
% 1.10/0.52 thf(f328,plain,(
% 1.10/0.52 ~(member @ a @ (g @ xa) @ h1)),
% 1.10/0.52 inference(rectify,[],[f287])).
% 1.10/0.52 thf(f329,plain,(
% 1.10/0.52 ~ (((member @ a @ (g @ xa) @ h1)) = $true)),
% 1.10/0.52 inference(fool_elimination,[],[f328])).
% 1.10/0.52 thf(f378,plain,(
% 1.10/0.52 ! [X0 : nat] : ((ord_less @ nat @ zero_zero @ nat @ X0) => (((suc @ (minus_minus @ nat @ X0 @ (suc @ zero_zero @ nat)))) = X0))),
% 1.10/0.52 inference(rectify,[],[f27])).
% 1.10/0.52 thf(f379,plain,(
% 1.10/0.52 ! [X0 : nat] : ((((ord_less @ nat @ zero_zero @ nat @ X0)) = $true) => (((suc @ (minus_minus @ nat @ X0 @ (suc @ zero_zero @ nat)))) = X0))),
% 1.10/0.52 inference(fool_elimination,[],[f378])).
% 1.10/0.52 thf(f460,plain,(
% 1.10/0.52 (ord_less @ nat @ zero_zero @ nat @ m2)),
% 1.10/0.52 inference(rectify,[],[f281])).
% 1.10/0.52 thf(f461,plain,(
% 1.10/0.52 (((ord_less @ nat @ zero_zero @ nat @ m2)) = $true)),
% 1.10/0.52 inference(fool_elimination,[],[f460])).
% 1.10/0.52 thf(f484,plain,(
% 1.10/0.52 (member @ a @ (g @ xa) @ h1) | (((g @ xa)) = h2)),
% 1.10/0.52 inference(rectify,[],[f285])).
% 1.10/0.52 thf(f485,plain,(
% 1.10/0.52 (h2 = ((g @ xa))) | (((member @ a @ (g @ xa) @ h1)) = $true)),
% 1.10/0.52 inference(fool_elimination,[],[f484])).
% 1.10/0.52 thf(f488,plain,(
% 1.10/0.52 ! [X0 : nat,X1 : nat,X2 : nat] : ((ord_less_eq @ nat @ X0 @ X1) => ((ord_less_eq @ nat @ X1 @ X2) => (ord_less_eq @ nat @ X0 @ X2)))),
% 1.10/0.52 inference(rectify,[],[f71])).
% 1.10/0.52 thf(f489,plain,(
% 1.10/0.52 ! [X2 : nat,X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ X1)) = $true) => ((((ord_less_eq @ nat @ X1 @ X2)) = $true) => (((ord_less_eq @ nat @ X0 @ X2)) = $true)))),
% 1.10/0.52 inference(fool_elimination,[],[f488])).
% 1.10/0.52 thf(f619,plain,(
% 1.10/0.52 ! [X0 : nat] : ((ord_less_eq @ nat @ X0 @ m2) => ! [X1 : nat] : ((ord_less_eq @ nat @ X1 @ m2) => ((((g @ X0)) = ((g @ X1))) => (X0 = X1))))),
% 1.10/0.52 inference(rectify,[],[f266])).
% 1.10/0.52 thf(f620,plain,(
% 1.10/0.52 ! [X0 : nat] : ((((ord_less_eq @ nat @ X0 @ m2)) = $true) => ! [X1 : nat] : ((((ord_less_eq @ nat @ X1 @ m2)) = $true) => ((((g @ X0)) = ((g @ X1))) => (X0 = X1))))),
% 1.10/0.52 inference(fool_elimination,[],[f619])).
% 1.10/0.52 thf(f724,plain,(
% 1.10/0.52 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X1 @ X0) | (ord_less_eq @ nat @ X0 @ X1))),
% 1.10/0.52 inference(rectify,[],[f69])).
% 1.10/0.52 thf(f725,plain,(
% 1.10/0.52 ! [X1 : nat,X0 : nat] : ((((ord_less_eq @ nat @ X1 @ X0)) = $true) | (((ord_less_eq @ nat @ X0 @ X1)) = $true))),
% 1.10/0.52 inference(fool_elimination,[],[f724])).
% 1.10/0.52 thf(f785,plain,(
% 1.10/0.52 (((member @ a @ (g @ xa) @ h1)) != $true)),
% 1.10/0.52 inference(flattening,[],[f329])).
% 1.10/0.52 thf(f862,plain,(
% 1.10/0.52 ! [X2 : nat,X0 : nat,X1 : nat] : (((((ord_less_eq @ nat @ X0 @ X2)) = $true) | (((ord_less_eq @ nat @ X1 @ X2)) != $true)) | (((ord_less_eq @ nat @ X0 @ X1)) != $true))),
% 1.10/0.52 inference(ennf_transformation,[],[f489])).
% 1.10/0.52 thf(f863,plain,(
% 1.10/0.52 ! [X0 : nat,X1 : nat,X2 : nat] : ((((ord_less_eq @ nat @ X0 @ X2)) = $true) | (((ord_less_eq @ nat @ X1 @ X2)) != $true) | (((ord_less_eq @ nat @ X0 @ X1)) != $true))),
% 1.10/0.52 inference(flattening,[],[f862])).
% 1.10/0.52 thf(f864,plain,(
% 1.10/0.52 ! [X0 : nat] : (! [X1 : nat] : (((X0 = X1) | (((g @ X0)) != ((g @ X1)))) | (((ord_less_eq @ nat @ X1 @ m2)) != $true)) | (((ord_less_eq @ nat @ X0 @ m2)) != $true))),
% 1.10/0.52 inference(ennf_transformation,[],[f620])).
% 1.10/0.52 thf(f865,plain,(
% 1.10/0.52 ! [X0 : nat] : ((((ord_less_eq @ nat @ X0 @ m2)) != $true) | ! [X1 : nat] : ((((g @ X0)) != ((g @ X1))) | (X0 = X1) | (((ord_less_eq @ nat @ X1 @ m2)) != $true)))),
% 1.10/0.52 inference(flattening,[],[f864])).
% 1.10/0.52 thf(f1046,plain,(
% 1.10/0.52 ! [X0 : nat,X1 : nat] : (((X0 = X1) | (((ord_less_eq @ nat @ X1 @ X0)) != $true)) | (((ord_less_eq @ nat @ X0 @ X1)) != $true))),
% 1.10/0.52 inference(ennf_transformation,[],[f315])).
% 1.10/0.52 thf(f1047,plain,(
% 1.10/0.52 ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ X1)) != $true) | (X0 = X1) | (((ord_less_eq @ nat @ X1 @ X0)) != $true))),
% 1.10/0.52 inference(flattening,[],[f1046])).
% 1.10/0.52 thf(f1089,plain,(
% 1.10/0.52 ! [X0 : nat] : ((((suc @ (minus_minus @ nat @ X0 @ (suc @ zero_zero @ nat)))) = X0) | (((ord_less @ nat @ zero_zero @ nat @ X0)) != $true))),
% 1.10/0.52 inference(ennf_transformation,[],[f379])).
% 1.10/0.52 thf(f1128,plain,(
% 1.10/0.52 ! [X0 : nat,X1 : nat] : (((ord_less_eq @ nat @ (minus_minus @ nat @ X1 @ X0) @ X1)) = $true)),
% 1.10/0.52 inference(rectify,[],[f297])).
% 1.10/0.52 thf(f1144,plain,(
% 1.10/0.52 ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ X1)) = $true) | (((ord_less_eq @ nat @ X1 @ X0)) = $true))),
% 1.10/0.52 inference(rectify,[],[f725])).
% 1.10/0.52 thf(f1326,plain,(
% 1.10/0.52 ( ! [X0 : nat] : ((((minus_minus @ nat @ X0 @ zero_zero @ nat)) = X0)) )),
% 1.10/0.52 inference(cnf_transformation,[],[f152])).
% 1.10/0.52 thf(f1333,plain,(
% 1.10/0.52 (((ord_less_eq @ nat @ xa @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)))) = $true)),
% 1.10/0.52 inference(cnf_transformation,[],[f323])).
% 1.10/0.52 thf(f1389,plain,(
% 1.10/0.52 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ (minus_minus @ nat @ X1 @ X0) @ X1)) = $true)) )),
% 1.10/0.52 inference(cnf_transformation,[],[f1128])).
% 1.10/0.52 thf(f1414,plain,(
% 1.10/0.52 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ X0)) = $true) | (((ord_less_eq @ nat @ X0 @ X1)) = $true)) )),
% 1.10/0.52 inference(cnf_transformation,[],[f1144])).
% 1.10/0.52 thf(f1416,plain,(
% 1.10/0.52 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ X0)) != $true) | (X0 = X1) | (((ord_less_eq @ nat @ X0 @ X1)) != $true)) )),
% 1.10/0.52 inference(cnf_transformation,[],[f1047])).
% 1.10/0.52 thf(f1417,plain,(
% 1.10/0.52 (((member @ a @ (g @ xa) @ h1)) != $true)),
% 1.10/0.52 inference(cnf_transformation,[],[f785])).
% 1.10/0.52 thf(f1438,plain,(
% 1.10/0.52 (((ord_less @ nat @ zero_zero @ nat @ m2)) = $true)),
% 1.10/0.52 inference(cnf_transformation,[],[f461])).
% 1.10/0.52 thf(f1452,plain,(
% 1.10/0.52 ( ! [X0 : nat] : ((((suc @ X0)) != X0)) )),
% 1.10/0.52 inference(cnf_transformation,[],[f72])).
% 1.10/0.52 thf(f1476,plain,(
% 1.10/0.52 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ m2)) != $true) | (((g @ X0)) != ((g @ X1))) | (((ord_less_eq @ nat @ X0 @ m2)) != $true) | (X0 = X1)) )),
% 1.10/0.52 inference(cnf_transformation,[],[f865])).
% 1.10/0.52 thf(f1486,plain,(
% 1.10/0.52 ( ! [X2 : nat,X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ X2)) = $true) | (((ord_less_eq @ nat @ X1 @ X2)) != $true) | (((ord_less_eq @ nat @ X0 @ X1)) != $true)) )),
% 1.10/0.52 inference(cnf_transformation,[],[f863])).
% 1.10/0.52 thf(f1579,plain,(
% 1.10/0.52 ( ! [X0 : nat] : ((((suc @ (minus_minus @ nat @ X0 @ (suc @ zero_zero @ nat)))) = X0) | (((ord_less @ nat @ zero_zero @ nat @ X0)) != $true)) )),
% 1.10/0.52 inference(cnf_transformation,[],[f1089])).
% 1.10/0.52 thf(f1654,plain,(
% 1.10/0.52 (h2 = ((g @ m2)))),
% 1.10/0.52 inference(cnf_transformation,[],[f268])).
% 1.10/0.52 thf(f1706,plain,(
% 1.10/0.52 (((member @ a @ (g @ xa) @ h1)) = $true) | (h2 = ((g @ xa)))),
% 1.10/0.52 inference(cnf_transformation,[],[f485])).
% 1.10/0.52 thf(f1871,definition,(
% 1.10/0.52 spl79_16 <=> (((ord_less @ nat @ zero_zero @ nat @ m2)) = $true)),
% 1.10/0.52 introduced(definition,[new_symbols(definition,[spl79_16])],[avatar_definition])).
% 1.10/0.52 thf(f1873,plain,(
% 1.10/0.52 (((ord_less @ nat @ zero_zero @ nat @ m2)) = $true) | ~spl79_16),
% 1.10/0.52 inference(avatar_component_clause,[],[f1871])).
% 1.10/0.52 thf(f1874,plain,(
% 1.10/0.52 spl79_16),
% 1.10/0.52 inference(avatar_split_clause,[],[f1438,f1871])).
% 1.10/0.52 thf(f1911,definition,(
% 1.10/0.52 spl79_24 <=> (((member @ a @ (g @ xa) @ h1)) = $true)),
% 1.10/0.52 introduced(definition,[new_symbols(definition,[spl79_24])],[avatar_definition])).
% 1.10/0.52 thf(f1914,plain,(
% 1.10/0.52 ~spl79_24),
% 1.10/0.52 inference(avatar_split_clause,[],[f1417,f1911])).
% 1.10/0.52 thf(f1931,definition,(
% 1.10/0.52 spl79_28 <=> (((ord_less_eq @ nat @ xa @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)))) = $true)),
% 1.10/0.52 introduced(definition,[new_symbols(definition,[spl79_28])],[avatar_definition])).
% 1.10/0.52 thf(f1933,plain,(
% 1.10/0.52 (((ord_less_eq @ nat @ xa @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)))) = $true) | ~spl79_28),
% 1.10/0.52 inference(avatar_component_clause,[],[f1931])).
% 1.10/0.52 thf(f1934,plain,(
% 1.10/0.52 spl79_28),
% 1.10/0.52 inference(avatar_split_clause,[],[f1333,f1931])).
% 1.10/0.52 thf(f1956,definition,(
% 1.10/0.52 spl79_33 <=> (h2 = ((g @ xa)))),
% 1.10/0.52 introduced(definition,[new_symbols(definition,[spl79_33])],[avatar_definition])).
% 1.10/0.52 thf(f1958,plain,(
% 1.10/0.52 (h2 = ((g @ xa))) | ~spl79_33),
% 1.10/0.52 inference(avatar_component_clause,[],[f1956])).
% 1.10/0.52 thf(f1959,plain,(
% 1.10/0.52 spl79_33 | spl79_24),
% 1.10/0.52 inference(avatar_split_clause,[],[f1706,f1911,f1956])).
% 1.10/0.52 thf(f1961,definition,(
% 1.10/0.52 spl79_34 <=> (h2 = ((g @ m2)))),
% 1.10/0.52 introduced(definition,[new_symbols(definition,[spl79_34])],[avatar_definition])).
% 1.10/0.52 thf(f1963,plain,(
% 1.10/0.52 (h2 = ((g @ m2))) | ~spl79_34),
% 1.10/0.52 inference(avatar_component_clause,[],[f1961])).
% 1.10/0.52 thf(f1964,plain,(
% 1.10/0.52 spl79_34),
% 1.10/0.52 inference(avatar_split_clause,[],[f1654,f1961])).
% 1.10/0.52 thf(f2097,plain,(
% 1.10/0.52 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ m2)) != $true) | ($true != $true) | (((g @ X1)) != ((g @ (minus_minus @ nat @ m2 @ X0)))) | (((minus_minus @ nat @ m2 @ X0)) = X1)) )),
% 1.10/0.52 inference(superposition,[],[f1476,f1389])).
% 1.10/0.52 thf(f2099,plain,(
% 1.10/0.52 ( ! [X0 : nat,X1 : nat] : ((((g @ X1)) != ((g @ (minus_minus @ nat @ m2 @ X0)))) | (((ord_less_eq @ nat @ X1 @ m2)) != $true) | (((minus_minus @ nat @ m2 @ X0)) = X1)) )),
% 1.10/0.52 inference(trivial_inequality_removal,[],[f2097])).
% 1.10/0.52 thf(f2102,plain,(
% 1.10/0.52 ( ! [X0 : nat] : ((((g @ X0)) != ((g @ m2))) | (((ord_less_eq @ nat @ X0 @ m2)) != $true) | (m2 = X0)) )),
% 1.10/0.52 inference(superposition,[],[f2099,f1326])).
% 1.10/0.52 thf(f2110,definition,(
% 1.10/0.52 spl79_54 <=> (((ord_less_eq @ nat @ xa @ m2)) = $true)),
% 1.10/0.52 introduced(definition,[new_symbols(definition,[spl79_54])],[avatar_definition])).
% 1.10/0.52 thf(f2111,plain,(
% 1.10/0.52 (((ord_less_eq @ nat @ xa @ m2)) = $true) | ~spl79_54),
% 1.10/0.52 inference(avatar_component_clause,[],[f2110])).
% 1.10/0.52 thf(f2112,plain,(
% 1.10/0.52 (((ord_less_eq @ nat @ xa @ m2)) != $true) | spl79_54),
% 1.10/0.52 inference(avatar_component_clause,[],[f2110])).
% 1.10/0.52 thf(f2204,definition,(
% 1.10/0.52 spl79_63 <=> ! [X0 : nat] : ((((ord_less_eq @ nat @ X0 @ m2)) != $true) | (m2 = X0) | (((g @ X0)) != ((g @ m2))))),
% 1.10/0.52 introduced(definition,[new_symbols(definition,[spl79_63])],[avatar_definition])).
% 1.10/0.52 thf(f2205,plain,(
% 1.10/0.52 ( ! [X0 : nat] : ((((ord_less_eq @ nat @ X0 @ m2)) != $true) | (m2 = X0) | (((g @ X0)) != ((g @ m2)))) ) | ~spl79_63),
% 1.10/0.52 inference(avatar_component_clause,[],[f2204])).
% 1.10/0.52 thf(f2237,plain,(
% 1.10/0.52 (xa = ((minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)))) | ($true != $true) | (((ord_less_eq @ nat @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)) @ xa)) != $true) | ~spl79_28),
% 1.10/0.52 inference(superposition,[],[f1416,f1933])).
% 1.10/0.52 thf(f2240,plain,(
% 1.10/0.52 (((ord_less_eq @ nat @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)) @ xa)) != $true) | (xa = ((minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)))) | ~spl79_28),
% 1.10/0.52 inference(trivial_inequality_removal,[],[f2237])).
% 1.10/0.52 thf(f2243,definition,(
% 1.10/0.52 spl79_66 <=> (xa = ((minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat))))),
% 1.10/0.52 introduced(definition,[new_symbols(definition,[spl79_66])],[avatar_definition])).
% 1.10/0.52 thf(f2245,plain,(
% 1.10/0.52 (xa = ((minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)))) | ~spl79_66),
% 1.10/0.52 inference(avatar_component_clause,[],[f2243])).
% 1.10/0.52 thf(f2247,definition,(
% 1.10/0.52 spl79_67 <=> (((ord_less_eq @ nat @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)) @ xa)) = $true)),
% 1.10/0.52 introduced(definition,[new_symbols(definition,[spl79_67])],[avatar_definition])).
% 1.10/0.52 thf(f2249,plain,(
% 1.10/0.52 (((ord_less_eq @ nat @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)) @ xa)) != $true) | spl79_67),
% 1.10/0.52 inference(avatar_component_clause,[],[f2247])).
% 1.10/0.52 thf(f2250,plain,(
% 1.10/0.52 spl79_66 | ~spl79_67 | ~spl79_28),
% 1.10/0.52 inference(avatar_split_clause,[],[f2240,f1931,f2247,f2243])).
% 1.10/0.52 thf(f2368,plain,(
% 1.10/0.52 spl79_63),
% 1.10/0.52 inference(avatar_split_clause,[],[f2102,f2204])).
% 1.10/0.52 thf(f2813,plain,(
% 1.10/0.52 ($true != $true) | ($true = ((ord_less_eq @ nat @ m2 @ xa))) | spl79_54),
% 1.10/0.52 inference(superposition,[],[f2112,f1414])).
% 1.10/0.52 thf(f2814,plain,(
% 1.10/0.52 ($true = ((ord_less_eq @ nat @ m2 @ xa))) | spl79_54),
% 1.10/0.52 inference(trivial_inequality_removal,[],[f2813])).
% 1.10/0.52 thf(f2816,definition,(
% 1.10/0.52 spl79_86 <=> ($true = ((ord_less_eq @ nat @ m2 @ xa)))),
% 1.10/0.52 introduced(definition,[new_symbols(definition,[spl79_86])],[avatar_definition])).
% 1.10/0.52 thf(f2818,plain,(
% 1.10/0.52 ($true = ((ord_less_eq @ nat @ m2 @ xa))) | ~spl79_86),
% 1.10/0.52 inference(avatar_component_clause,[],[f2816])).
% 1.10/0.52 thf(f2819,plain,(
% 1.10/0.52 spl79_86 | spl79_54),
% 1.10/0.52 inference(avatar_split_clause,[],[f2814,f2110,f2816])).
% 1.10/0.52 thf(f2821,plain,(
% 1.10/0.52 (m2 = xa) | (((g @ m2)) != ((g @ xa))) | ($true != $true) | (~spl79_54 | ~spl79_63)),
% 1.10/0.52 inference(superposition,[],[f2205,f2111])).
% 1.10/0.52 thf(f2827,plain,(
% 1.10/0.52 (m2 = xa) | (((g @ m2)) != ((g @ xa))) | (~spl79_54 | ~spl79_63)),
% 1.10/0.52 inference(trivial_inequality_removal,[],[f2821])).
% 1.10/0.52 thf(f2831,plain,(
% 1.10/0.52 (m2 = xa) | (h2 != ((g @ m2))) | (~spl79_33 | ~spl79_54 | ~spl79_63)),
% 1.10/0.52 inference(forward_demodulation,[],[f2827,f1958])).
% 1.10/0.52 thf(f2833,definition,(
% 1.10/0.52 spl79_87 <=> (m2 = xa)),
% 1.10/0.52 introduced(definition,[new_symbols(definition,[spl79_87])],[avatar_definition])).
% 1.10/0.52 thf(f2835,plain,(
% 1.10/0.52 (m2 = xa) | ~spl79_87),
% 1.10/0.52 inference(avatar_component_clause,[],[f2833])).
% 1.10/0.52 thf(f2839,plain,(
% 1.10/0.52 (m2 = xa) | (~spl79_33 | ~spl79_34 | ~spl79_54 | ~spl79_63)),
% 1.10/0.52 inference(forward_subsumption_resolution,[],[f2831,f1963])).
% 1.10/0.52 thf(f2841,plain,(
% 1.10/0.52 spl79_87 | ~spl79_33 | ~spl79_34 | ~spl79_54 | ~spl79_63),
% 1.10/0.52 inference(avatar_split_clause,[],[f2839,f2204,f2110,f1961,f1956,f2833])).
% 1.10/0.52 thf(f2877,plain,(
% 1.10/0.52 (((ord_less_eq @ nat @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)) @ m2)) != $true) | (spl79_67 | ~spl79_87)),
% 1.10/0.52 inference(superposition,[],[f2249,f2835])).
% 1.10/0.52 thf(f2884,plain,(
% 1.10/0.52 $false | (spl79_67 | ~spl79_87)),
% 1.10/0.52 inference(forward_subsumption_resolution,[],[f2877,f1389])).
% 1.10/0.52 thf(f2885,plain,(
% 1.10/0.52 spl79_67 | ~spl79_87),
% 1.10/0.52 inference(avatar_contradiction_clause,[],[f2884])).
% 1.10/0.52 thf(f2888,plain,(
% 1.10/0.52 (m2 = ((minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)))) | (~spl79_66 | ~spl79_87)),
% 1.10/0.52 inference(forward_demodulation,[],[f2245,f2835])).
% 1.10/0.52 thf(f2890,definition,(
% 1.10/0.52 spl79_90 <=> (m2 = ((minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat))))),
% 1.10/0.52 introduced(definition,[new_symbols(definition,[spl79_90])],[avatar_definition])).
% 1.10/0.52 thf(f2892,plain,(
% 1.10/0.52 (m2 = ((minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)))) | ~spl79_90),
% 1.10/0.52 inference(avatar_component_clause,[],[f2890])).
% 1.10/0.52 thf(f2893,plain,(
% 1.10/0.52 spl79_90 | ~spl79_66 | ~spl79_87),
% 1.10/0.52 inference(avatar_split_clause,[],[f2888,f2833,f2243,f2890])).
% 1.10/0.52 thf(f3016,plain,(
% 1.10/0.52 (m2 = ((suc @ m2))) | (((ord_less @ nat @ zero_zero @ nat @ m2)) != $true) | ~spl79_90),
% 1.10/0.52 inference(superposition,[],[f1579,f2892])).
% 1.10/0.52 thf(f3057,plain,(
% 1.10/0.52 (((ord_less @ nat @ zero_zero @ nat @ m2)) != $true) | ~spl79_90),
% 1.10/0.52 inference(forward_subsumption_resolution,[],[f3016,f1452])).
% 1.10/0.52 thf(f3058,plain,(
% 1.10/0.52 $false | (~spl79_16 | ~spl79_90)),
% 1.10/0.52 inference(forward_subsumption_resolution,[],[f3057,f1873])).
% 1.10/0.52 thf(f3059,plain,(
% 1.10/0.52 ~spl79_16 | ~spl79_90),
% 1.10/0.52 inference(avatar_contradiction_clause,[],[f3058])).
% 1.10/0.52 thf(f3506,plain,(
% 1.10/0.52 ( ! [X0 : nat] : (($true != $true) | (((ord_less_eq @ nat @ X0 @ xa)) != $true) | (((ord_less_eq @ nat @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)) @ X0)) != $true)) ) | spl79_67),
% 1.10/0.52 inference(superposition,[],[f2249,f1486])).
% 1.10/0.52 thf(f3525,plain,(
% 1.10/0.52 ( ! [X0 : nat] : ((((ord_less_eq @ nat @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)) @ X0)) != $true) | (((ord_less_eq @ nat @ X0 @ xa)) != $true)) ) | spl79_67),
% 1.10/0.52 inference(trivial_inequality_removal,[],[f3506])).
% 1.10/0.52 thf(f3731,plain,(
% 1.10/0.52 ($true != ((ord_less_eq @ nat @ m2 @ xa))) | ($true != $true) | spl79_67),
% 1.10/0.52 inference(superposition,[],[f3525,f1389])).
% 1.10/0.52 thf(f3737,plain,(
% 1.10/0.52 ($true != ((ord_less_eq @ nat @ m2 @ xa))) | spl79_67),
% 1.10/0.52 inference(trivial_inequality_removal,[],[f3731])).
% 1.10/0.52 thf(f3742,plain,(
% 1.10/0.52 $false | (spl79_67 | ~spl79_86)),
% 1.10/0.52 inference(forward_subsumption_resolution,[],[f3737,f2818])).
% 1.10/0.52 thf(f3743,plain,(
% 1.10/0.52 spl79_67 | ~spl79_86),
% 1.10/0.52 inference(avatar_contradiction_clause,[],[f3742])).
% 1.10/0.52 thf(f3821,plain,(
% 1.10/0.52 (((ord_less_eq @ nat @ (minus_minus @ nat @ m2 @ (suc @ zero_zero @ nat)) @ m2)) != $true) | (spl79_54 | ~spl79_66)),
% 1.10/0.52 inference(superposition,[],[f2112,f2245])).
% 1.10/0.52 thf(f3858,plain,(
% 1.10/0.52 $false | (spl79_54 | ~spl79_66)),
% 1.10/0.52 inference(forward_subsumption_resolution,[],[f3821,f1389])).
% 1.10/0.52 thf(f3859,plain,(
% 1.10/0.52 spl79_54 | ~spl79_66),
% 1.10/0.52 inference(avatar_contradiction_clause,[],[f3858])).
% 1.10/0.52 cnf(s16, plain, spl79_16, inference(sat_conversion,[],[f1874])).
% 1.10/0.52 cnf(s24, plain, ~spl79_24, inference(sat_conversion,[],[f1914])).
% 1.10/0.52 cnf(s28, plain, spl79_28, inference(sat_conversion,[],[f1934])).
% 1.10/0.52 cnf(s34, plain, spl79_24 | spl79_33, inference(sat_conversion,[],[f1959])).
% 1.10/0.52 cnf(s35, plain, spl79_34, inference(sat_conversion,[],[f1964])).
% 1.10/0.52 cnf(s65, plain, ~spl79_28 | spl79_66 | ~spl79_67, inference(sat_conversion,[],[f2250])).
% 1.10/0.52 cnf(s75, plain, spl79_63, inference(sat_conversion,[],[f2368])).
% 1.10/0.52 cnf(s117, plain, spl79_54 | spl79_86, inference(sat_conversion,[],[f2819])).
% 1.10/0.52 cnf(s119, plain, ~spl79_33 | ~spl79_34 | ~spl79_54 | ~spl79_63 | spl79_87, inference(sat_conversion,[],[f2841])).
% 1.10/0.52 cnf(s127, plain, spl79_67 | ~spl79_87, inference(sat_conversion,[],[f2885])).
% 1.10/0.52 cnf(s129, plain, ~spl79_66 | ~spl79_87 | spl79_90, inference(sat_conversion,[],[f2893])).
% 1.10/0.52 cnf(s136, plain, ~spl79_16 | ~spl79_90, inference(sat_conversion,[],[f3059])).
% 1.10/0.52 cnf(s161, plain, spl79_67 | ~spl79_86, inference(sat_conversion,[],[f3743])).
% 1.10/0.52 cnf(s170, plain, spl79_54 | ~spl79_66, inference(sat_conversion,[],[f3859])).
% 1.10/0.52 cnf(s175, plain, spl79_33, inference(rat,[],[s34,s24])).
% 1.10/0.52 cnf(s179, plain, ~spl79_90, inference(rat,[],[s136,s16])).
% 1.10/0.52 cnf(s206, plain, spl79_54, inference(rat,[],[s161,s65,s117,s170,s28])).
% 1.10/0.52 cnf(s207, plain, spl79_87, inference(rat,[],[s119,s175,s75,s35,s206])).
% 1.10/0.52 cnf(s211, plain, ~spl79_66, inference(rat,[],[s129,s179,s207])).
% 1.10/0.52 cnf(s212, plain, spl79_67, inference(rat,[],[s127,s207])).
% 1.10/0.52 cnf(s215, plain, $false, inference(rat,[],[s65,s28,s212,s211])).
% 1.10/0.52 thf(f3865,plain,(
% 1.10/0.52 $false),
% 1.10/0.52 inference(avatar_sat_refutation,[],[s215])).
% 1.10/0.52 % SZS output end Proof for theBenchmark
% 1.10/0.52 % (2113350)------------------------------
% 1.10/0.52 % (2113350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.52 % (2113350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.52 % (2113350)CaDiCaL version: 2.1.3
% 1.10/0.52 % (2113350)Termination reason: Refutation
% 1.10/0.52 % (2113350)Time elapsed: 0.177 s
% 1.10/0.52 % (2113350)Peak memory usage: 15 MB
% 1.10/0.52 % (2113350)Instructions burned: 335 (million)
% 1.10/0.52 % (2113342)Success in time 0.232 s
% 1.10/0.52 % Vampire exiting
%------------------------------------------------------------------------------