%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP108^1 : 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 : n017.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:22 AM UTC 2026
% Result : Theorem 0.29s 0.39s
% Output : Refutation 0.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP108^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n017.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 19:49:52 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running higher-order theorem proving
% 0.21/0.29 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.29/0.39 % (813198)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.29/0.39 % (813206)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=3308213610: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.29/0.39 % (813203)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2648999534:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.29/0.39 % (813205)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2870776640:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.29/0.39 % (813207)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3065444014:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.29/0.39 % (813209)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.29/0.39 % (813209)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.29/0.39 % (813204)lrs+10_16_si=on:nwc=1.5:random_seed=3851450403:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.29/0.39 % (813205)Instruction limit reached!
% 0.29/0.39 % (813205)------------------------------
% 0.29/0.39 % (813205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.39 % (813205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.39 % (813205)CaDiCaL version: 2.1.3
% 0.29/0.39 % (813205)Termination reason: Instruction limit
% 0.29/0.39 % (813205)Termination phase: shuffling
% 0.29/0.39 % (813205)Time elapsed: 0.002 s
% 0.29/0.39 % (813205)Peak memory usage: 10 MB
% 0.29/0.39 % (813205)Instructions burned: 4 (million)
% 0.29/0.39 % (813209)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=249234632:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.29/0.39 % (813207)Instruction limit reached!
% 0.29/0.39 % (813207)------------------------------
% 0.29/0.39 % (813207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.39 % (813207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.39 % (813207)CaDiCaL version: 2.1.3
% 0.29/0.39 % (813207)Termination reason: Instruction limit
% 0.29/0.39 % (813207)Termination phase: Property scanning
% 0.29/0.39 % (813207)Time elapsed: 0.010 s
% 0.29/0.39 % (813207)Peak memory usage: 10 MB
% 0.29/0.39 % (813207)Instructions burned: 25 (million)
% 0.29/0.39 % (813204)Instruction limit reached!
% 0.29/0.39 % (813204)------------------------------
% 0.29/0.39 % (813204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.39 % (813204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.39 % (813204)CaDiCaL version: 2.1.3
% 0.29/0.39 % (813204)Termination reason: Instruction limit
% 0.29/0.39 % (813204)Termination phase: Property scanning
% 0.29/0.39 % (813204)Time elapsed: 0.008 s
% 0.29/0.39 % (813204)Peak memory usage: 10 MB
% 0.29/0.39 % (813204)Instructions burned: 20 (million)
% 0.29/0.39 % (813208)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1772817236:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.29/0.39 % (813215)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1717910005:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.29/0.39 % (813215)Instruction limit reached!
% 0.29/0.39 % (813215)------------------------------
% 0.29/0.39 % (813215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.39 % (813215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.39 % (813215)CaDiCaL version: 2.1.3
% 0.29/0.39 % (813215)Termination reason: Instruction limit
% 0.29/0.39 % (813215)Termination phase: shuffling
% 0.29/0.39 % (813215)Time elapsed: 0.002 s
% 0.29/0.39 % (813215)Peak memory usage: 10 MB
% 0.29/0.39 % (813215)Instructions burned: 4 (million)
% 0.29/0.39 % (813218)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.29/0.39 % (813217)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3188907375:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.29/0.39 % (813218)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4113526332:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.29/0.39 % (813206) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-813198-813206"...
% 0.29/0.39 % (813217)Instruction limit reached!
% 0.29/0.39 % (813217)------------------------------
% 0.29/0.39 % (813217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.39 % (813217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.39 % (813217)CaDiCaL version: 2.1.3
% 0.29/0.39 % (813217)Termination reason: Instruction limit
% 0.29/0.39 % (813217)Termination phase: shuffling
% 0.29/0.39 % (813217)Time elapsed: 0.003 s
% 0.29/0.39 % (813217)Peak memory usage: 10 MB
% 0.29/0.39 % (813217)Instructions burned: 6 (million)
% 0.29/0.39 % (813206)...printing done.
% 0.29/0.39 % (813218)Instruction limit reached!
% 0.29/0.39 % (813218)------------------------------
% 0.29/0.39 % (813218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.39 % (813218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.39 % (813218)CaDiCaL version: 2.1.3
% 0.29/0.39 % (813218)Termination reason: Instruction limit
% 0.29/0.39 % (813218)Termination phase: shuffling
% 0.29/0.39 % (813218)Time elapsed: 0.004 s
% 0.29/0.39 % (813218)Peak memory usage: 10 MB
% 0.29/0.39 % (813218)Instructions burned: 9 (million)
% 0.29/0.39 % (813206)Refutation found. Thanks to Tanya!
% 0.29/0.39 % SZS status Theorem for theBenchmark
% 0.29/0.39 % SZS output start Proof for theBenchmark
% 0.29/0.39 thf(type_def_5, type, partia1833973666xt_a_b: $tType).
% 0.29/0.39 thf(type_def_6, type, product_prod_a_a: $tType).
% 0.29/0.39 thf(type_def_7, type, set_a: $tType).
% 0.29/0.39 thf(type_def_8, type, int: $tType).
% 0.29/0.39 thf(type_def_9, type, a: $tType).
% 0.29/0.39 thf(type_def_10, type, sTfun: ($tType * $tType) > $tType).
% 0.29/0.39 thf(func_def_0, type, a_l_coset_a_b: (partia1833973666xt_a_b > a > set_a > set_a)).
% 0.29/0.39 thf(func_def_1, type, additi2104487374up_a_b: (set_a > partia1833973666xt_a_b > $o)).
% 0.29/0.39 thf(func_def_2, type, set_add_a_b: (partia1833973666xt_a_b > set_a > set_a > set_a)).
% 0.29/0.39 thf(func_def_3, type, partia1066395285xt_a_b: (partia1833973666xt_a_b > set_a)).
% 0.29/0.39 thf(func_def_4, type, mult_a_ring_ext_a_b: (partia1833973666xt_a_b > a > a > a)).
% 0.29/0.39 thf(func_def_5, type, minus_minus_int: (int > int > int)).
% 0.29/0.39 thf(func_def_6, type, minus_minus_set_a: (set_a > set_a > set_a)).
% 0.29/0.39 thf(func_def_7, type, plus_plus_int: (int > int > int)).
% 0.29/0.39 thf(func_def_8, type, uminus_uminus_int: (int > int)).
% 0.29/0.39 thf(func_def_9, type, uminus_uminus_set_a: (set_a > set_a)).
% 0.29/0.39 thf(func_def_10, type, locali1648887798ac_a_b: (partia1833973666xt_a_b > set_a > $o)).
% 0.29/0.39 thf(func_def_11, type, locali807230110ng_a_b: (partia1833973666xt_a_b > set_a > $o)).
% 0.29/0.39 thf(func_def_12, type, locali880295127ng_a_b: (partia1833973666xt_a_b > set_a > $o)).
% 0.29/0.39 thf(func_def_13, type, locali425460998xt_a_b: (partia1833973666xt_a_b > set_a > $o)).
% 0.29/0.39 thf(func_def_14, type, bot_bot_set_a: set_a).
% 0.29/0.39 thf(func_def_15, type, ord_less_eq_int: (int > int > $o)).
% 0.29/0.39 thf(func_def_16, type, ord_less_eq_set_a: (set_a > set_a > $o)).
% 0.29/0.39 thf(func_def_17, type, product_fst_a_a: (product_prod_a_a > a)).
% 0.29/0.39 thf(func_def_18, type, product_snd_a_a: (product_prod_a_a > a)).
% 0.29/0.39 thf(func_def_19, type, a_inv_a_b: (partia1833973666xt_a_b > a > a)).
% 0.29/0.39 thf(func_def_20, type, a_minus_a_b: (partia1833973666xt_a_b > a > a > a)).
% 0.29/0.39 thf(func_def_21, type, add_pow_a_b_int: (partia1833973666xt_a_b > int > a > a)).
% 0.29/0.39 thf(func_def_22, type, add_a_b: (partia1833973666xt_a_b > a > a > a)).
% 0.29/0.39 thf(func_def_23, type, zero_a_b: (partia1833973666xt_a_b > a)).
% 0.29/0.39 thf(func_def_24, type, semiring_a_b: (partia1833973666xt_a_b > $o)).
% 0.29/0.39 thf(func_def_25, type, collect_a: ((a > $o) > set_a)).
% 0.29/0.39 thf(func_def_26, type, member_a: (a > set_a > $o)).
% 0.29/0.39 thf(func_def_27, type, r: partia1833973666xt_a_b).
% 0.29/0.39 thf(func_def_28, type, s: set_a).
% 0.29/0.39 thf(func_def_29, type, r2: a).
% 0.29/0.39 thf(func_def_30, type, r3: a).
% 0.29/0.39 thf(func_def_31, type, s2: a).
% 0.29/0.39 thf(func_def_32, type, s3: a).
% 0.29/0.39 thf(func_def_33, type, t: a).
% 0.29/0.39 thf(func_def_34, type, t2: a).
% 0.29/0.39 thf(func_def_35, type, x: product_prod_a_a).
% 0.29/0.39 thf(func_def_36, type, y: product_prod_a_a).
% 0.29/0.39 thf(func_def_40, type, db1: !>[X0: $tType]:(X0)).
% 0.29/0.39 thf(func_def_41, type, db0: !>[X0: $tType]:(X0)).
% 0.29/0.39 thf(func_def_42, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.29/0.39 thf(func_def_43, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.29/0.39 thf(func_def_44, type, vAND: ($o > $o > $o)).
% 0.29/0.39 thf(func_def_45, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.29/0.39 thf(func_def_46, type, vIMP: ($o > $o > $o)).
% 0.29/0.39 thf(func_def_47, type, db2: !>[X0: $tType]:(X0)).
% 0.29/0.39 thf(func_def_48, type, sK0: a).
% 0.29/0.39 thf(func_def_49, type, sK1: (a > a)).
% 0.29/0.39 thf(func_def_50, type, sK2: (a > a)).
% 0.29/0.39 thf(func_def_51, type, sK3: (set_a > a)).
% 0.29/0.39 thf(func_def_52, type, sK4: (set_a > a)).
% 0.29/0.39 thf(func_def_53, type, sK5: (set_a > a)).
% 0.29/0.39 thf(func_def_54, type, sK6: ((a > $o) > a)).
% 0.29/0.39 thf(func_def_55, type, sK7: (set_a > a)).
% 0.29/0.39 thf(func_def_56, type, sK8: ((a > $o) > a)).
% 0.29/0.39 thf(func_def_57, type, sK9: (set_a > set_a > a)).
% 0.29/0.39 thf(func_def_58, type, sK10: a).
% 0.29/0.39 thf(func_def_59, type, sK11: ((a > a > $o) > a)).
% 0.29/0.39 thf(func_def_60, type, sK12: ((a > a > $o) > a)).
% 0.29/0.39 thf(func_def_61, type, sK13: (a > a)).
% 0.29/0.39 thf(func_def_62, type, sK14: (set_a > a)).
% 0.29/0.39 thf(func_def_63, type, sK15: ((a > $o) > (a > $o) > a)).
% 0.29/0.39 thf(func_def_64, type, sK16: (set_a > a)).
% 0.29/0.39 thf(func_def_65, type, vNOT: ($o > $o)).
% 0.29/0.39 thf(f1,axiom,(
% 0.29/0.39 (member_a @ t @ (partia1066395285xt_a_b @ r))),
% 0.29/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_f18)).
% 0.29/0.39 thf(f2,axiom,(
% 0.29/0.39 (member_a @ t2 @ (partia1066395285xt_a_b @ r))),
% 0.29/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_f17)).
% 0.29/0.39 thf(f13,axiom,(
% 0.29/0.39 (member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (partia1066395285xt_a_b @ r))),
% 0.29/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_f41)).
% 0.29/0.39 thf(f14,axiom,(
% 0.29/0.39 (member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))) @ (partia1066395285xt_a_b @ r))),
% 0.29/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_f42)).
% 0.29/0.39 thf(f20,axiom,(
% 0.29/0.39 (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t @ s3) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ t2 @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ r2) @ (mult_a_ring_ext_a_b @ r @ s2 @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ s2) @ (product_snd_a_a @ x)) @ (mult_a_ring_ext_a_b @ r @ t @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ r3) @ (mult_a_ring_ext_a_b @ r @ s3 @ (product_fst_a_a @ y))))))) = ((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))),
% 0.29/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_f40)).
% 0.29/0.39 thf(f22,axiom,(
% 0.29/0.39 (member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (partia1066395285xt_a_b @ r)) => ((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))) @ (partia1066395285xt_a_b @ r)) => ((member_a @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (partia1066395285xt_a_b @ r)) => (((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))) = ((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))))),
% 0.29/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21__092_060open_062_092_060lbrakk_062snd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ay_H_A_092_060otimes_062_Afst_Ax_H_J_A_092_060in_062_Acarrier_AR_059_Asnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Afst_Ay_H_J_A_092_060in_062_Acarrier_AR_059_At_A_092_060otimes_062_At_H_A_092_060in_062_Acarrier_AR_092_060rbrakk_062_A_092_060Longrightarrow_062_At_A_092_060otimes_062_At_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ay_H_A_092_060otimes_062_Afst_Ax_H_J_A_092_060oplus_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Afst_Ay_H_J_J_J_A_061_At_A_092_060otimes_062_At_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_H_A_092_060otimes_062_Ar_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ay_H_A_092_060otimes_062_Afst_Ax_H_J_J_A_092_060oplus_062_At_A_092_060otimes_062_At_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Asnd_Ay_H_A_092_060otimes_062_A_Is_A_092_060otimes_062_Ar_H_J_A_092_060ominus_062_As_A_092_060otimes_062_As_H_A_092_060otimes_062_A_Isnd_Ax_H_A_092_060otimes_062_Afst_Ay_H_J_J_092_060close_062)).
% 0.29/0.39 thf(f63,axiom,(
% 0.29/0.39 ! [X0 : a,X1 : a] : ((member_a @ X0 @ (partia1066395285xt_a_b @ r)) => ((member_a @ X1 @ (partia1066395285xt_a_b @ r)) => (member_a @ (mult_a_ring_ext_a_b @ r @ X0 @ X1) @ (partia1066395285xt_a_b @ r))))),
% 0.29/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_semiring__simprules_I3_J)).
% 0.29/0.39 thf(f245,conjecture,(
% 0.29/0.39 (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t @ s3) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ t2 @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ r2) @ (mult_a_ring_ext_a_b @ r @ s2 @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ s2) @ (product_snd_a_a @ x)) @ (mult_a_ring_ext_a_b @ r @ t @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ r3) @ (mult_a_ring_ext_a_b @ r @ s3 @ (product_fst_a_a @ y))))))) = ((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))),
% 0.29/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 0.29/0.39 thf(f246,negated_conjecture,(
% 0.29/0.39 ~ (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t @ s3) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ t2 @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ r2) @ (mult_a_ring_ext_a_b @ r @ s2 @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ s2) @ (product_snd_a_a @ x)) @ (mult_a_ring_ext_a_b @ r @ t @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ r3) @ (mult_a_ring_ext_a_b @ r @ s3 @ (product_fst_a_a @ y))))))) = ((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))),
% 0.29/0.39 inference(negated_conjecture,[status(cth)],[f245])).
% 0.29/0.39 thf(f255,plain,(
% 0.29/0.39 (member_a @ t2 @ (partia1066395285xt_a_b @ r))),
% 0.29/0.39 inference(rectify,[],[f2])).
% 0.29/0.39 thf(f256,plain,(
% 0.29/0.39 (((member_a @ t2 @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 inference(fool_elimination,[],[f255])).
% 0.29/0.39 thf(f268,plain,(
% 0.29/0.39 (member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))) @ (partia1066395285xt_a_b @ r))),
% 0.29/0.39 inference(rectify,[],[f14])).
% 0.29/0.39 thf(f269,plain,(
% 0.29/0.39 (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))) @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 inference(fool_elimination,[],[f268])).
% 0.29/0.39 thf(f368,plain,(
% 0.29/0.39 (member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (partia1066395285xt_a_b @ r)) => ((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))) @ (partia1066395285xt_a_b @ r)) => ((member_a @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (partia1066395285xt_a_b @ r)) => (((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))) = ((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))))),
% 0.29/0.39 inference(rectify,[],[f22])).
% 0.29/0.39 thf(f369,plain,(
% 0.29/0.39 (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (partia1066395285xt_a_b @ r))) = $true) => ((((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))) @ (partia1066395285xt_a_b @ r))) = $true) => ((((member_a @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (partia1066395285xt_a_b @ r))) = $true) => (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))) = ((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))))),
% 0.29/0.39 inference(fool_elimination,[],[f368])).
% 0.29/0.39 thf(f458,plain,(
% 0.29/0.39 (member_a @ t @ (partia1066395285xt_a_b @ r))),
% 0.29/0.39 inference(rectify,[],[f1])).
% 0.29/0.39 thf(f459,plain,(
% 0.29/0.39 (((member_a @ t @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 inference(fool_elimination,[],[f458])).
% 0.29/0.39 thf(f533,plain,(
% 0.29/0.39 (member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (partia1066395285xt_a_b @ r))),
% 0.29/0.39 inference(rectify,[],[f13])).
% 0.29/0.39 thf(f534,plain,(
% 0.29/0.39 (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 inference(fool_elimination,[],[f533])).
% 0.29/0.39 thf(f551,plain,(
% 0.29/0.39 ! [X0 : a,X1 : a] : ((member_a @ X0 @ (partia1066395285xt_a_b @ r)) => ((member_a @ X1 @ (partia1066395285xt_a_b @ r)) => (member_a @ (mult_a_ring_ext_a_b @ r @ X0 @ X1) @ (partia1066395285xt_a_b @ r))))),
% 0.29/0.39 inference(rectify,[],[f63])).
% 0.29/0.39 thf(f552,plain,(
% 0.29/0.39 ! [X0 : a,X1 : a] : ((((member_a @ X0 @ (partia1066395285xt_a_b @ r))) = $true) => ((((member_a @ X1 @ (partia1066395285xt_a_b @ r))) = $true) => (((member_a @ (mult_a_ring_ext_a_b @ r @ X0 @ X1) @ (partia1066395285xt_a_b @ r))) = $true)))),
% 0.29/0.39 inference(fool_elimination,[],[f551])).
% 0.29/0.39 thf(f611,plain,(
% 0.29/0.39 (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t @ s3) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ t2 @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ r2) @ (mult_a_ring_ext_a_b @ r @ s2 @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ s2) @ (product_snd_a_a @ x)) @ (mult_a_ring_ext_a_b @ r @ t @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ r3) @ (mult_a_ring_ext_a_b @ r @ s3 @ (product_fst_a_a @ y))))))) != ((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))),
% 0.29/0.39 inference(flattening,[],[f246])).
% 0.29/0.39 thf(f643,plain,(
% 0.29/0.39 (((((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))) = ((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))))))) | (((member_a @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (partia1066395285xt_a_b @ r))) != $true)) | (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))) @ (partia1066395285xt_a_b @ r))) != $true)) | (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (partia1066395285xt_a_b @ r))) != $true)),
% 0.29/0.39 inference(ennf_transformation,[],[f369])).
% 0.29/0.39 thf(f644,plain,(
% 0.29/0.39 (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))) @ (partia1066395285xt_a_b @ r))) != $true) | (((member_a @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (partia1066395285xt_a_b @ r))) != $true) | (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (partia1066395285xt_a_b @ r))) != $true) | (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))) = ((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))),
% 0.29/0.39 inference(flattening,[],[f643])).
% 0.29/0.39 thf(f777,plain,(
% 0.29/0.39 ! [X0 : a,X1 : a] : (((((member_a @ (mult_a_ring_ext_a_b @ r @ X0 @ X1) @ (partia1066395285xt_a_b @ r))) = $true) | (((member_a @ X1 @ (partia1066395285xt_a_b @ r))) != $true)) | (((member_a @ X0 @ (partia1066395285xt_a_b @ r))) != $true))),
% 0.29/0.39 inference(ennf_transformation,[],[f552])).
% 0.29/0.39 thf(f778,plain,(
% 0.29/0.39 ! [X1 : a,X0 : a] : ((((member_a @ X0 @ (partia1066395285xt_a_b @ r))) != $true) | (((member_a @ X1 @ (partia1066395285xt_a_b @ r))) != $true) | (((member_a @ (mult_a_ring_ext_a_b @ r @ X0 @ X1) @ (partia1066395285xt_a_b @ r))) = $true))),
% 0.29/0.39 inference(flattening,[],[f777])).
% 0.29/0.39 thf(f928,plain,(
% 0.29/0.39 ! [X0 : a,X1 : a] : ((((member_a @ X1 @ (partia1066395285xt_a_b @ r))) != $true) | (((member_a @ X0 @ (partia1066395285xt_a_b @ r))) != $true) | ($true = ((member_a @ (mult_a_ring_ext_a_b @ r @ X1 @ X0) @ (partia1066395285xt_a_b @ r)))))),
% 0.29/0.39 inference(rectify,[],[f778])).
% 0.29/0.39 thf(f1013,plain,(
% 0.29/0.39 (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 inference(cnf_transformation,[],[f534])).
% 0.29/0.39 thf(f1042,plain,(
% 0.29/0.39 (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t @ s3) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ t2 @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ r2) @ (mult_a_ring_ext_a_b @ r @ s2 @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ s2) @ (product_snd_a_a @ x)) @ (mult_a_ring_ext_a_b @ r @ t @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ r3) @ (mult_a_ring_ext_a_b @ r @ s3 @ (product_fst_a_a @ y))))))) = ((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))),
% 0.29/0.39 inference(cnf_transformation,[],[f20])).
% 0.29/0.39 thf(f1047,plain,(
% 0.29/0.39 (((member_a @ t2 @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 inference(cnf_transformation,[],[f256])).
% 0.29/0.39 thf(f1106,plain,(
% 0.29/0.39 (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (partia1066395285xt_a_b @ r))) != $true) | (((member_a @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (partia1066395285xt_a_b @ r))) != $true) | (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))) @ (partia1066395285xt_a_b @ r))) != $true) | (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))) = ((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))),
% 0.29/0.39 inference(cnf_transformation,[],[f644])).
% 0.29/0.39 thf(f1154,plain,(
% 0.29/0.39 (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))) @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 inference(cnf_transformation,[],[f269])).
% 0.29/0.39 thf(f1162,plain,(
% 0.29/0.39 ( ! [X0 : a,X1 : a] : (($true = ((member_a @ (mult_a_ring_ext_a_b @ r @ X1 @ X0) @ (partia1066395285xt_a_b @ r)))) | (((member_a @ X1 @ (partia1066395285xt_a_b @ r))) != $true) | (((member_a @ X0 @ (partia1066395285xt_a_b @ r))) != $true)) )),
% 0.29/0.39 inference(cnf_transformation,[],[f928])).
% 0.29/0.39 thf(f1189,plain,(
% 0.29/0.39 (((member_a @ t @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 inference(cnf_transformation,[],[f459])).
% 0.29/0.39 thf(f1208,plain,(
% 0.29/0.39 (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t @ s3) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ t2 @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ r2) @ (mult_a_ring_ext_a_b @ r @ s2 @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ s2) @ (product_snd_a_a @ x)) @ (mult_a_ring_ext_a_b @ r @ t @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ r3) @ (mult_a_ring_ext_a_b @ r @ s3 @ (product_fst_a_a @ y))))))) != ((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))),
% 0.29/0.39 inference(cnf_transformation,[],[f611])).
% 0.29/0.39 thf(f1331,definition,(
% 0.29/0.39 spl17_2 <=> (((member_a @ t2 @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl17_2])],[avatar_definition])).
% 0.29/0.39 thf(f1333,plain,(
% 0.29/0.39 (((member_a @ t2 @ (partia1066395285xt_a_b @ r))) = $true) | ~spl17_2),
% 0.29/0.39 inference(avatar_component_clause,[],[f1331])).
% 0.29/0.39 thf(f1334,plain,(
% 0.29/0.39 spl17_2),
% 0.29/0.39 inference(avatar_split_clause,[],[f1047,f1331])).
% 0.29/0.39 thf(f1380,definition,(
% 0.29/0.39 spl17_12 <=> (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl17_12])],[avatar_definition])).
% 0.29/0.39 thf(f1383,plain,(
% 0.29/0.39 spl17_12),
% 0.29/0.39 inference(avatar_split_clause,[],[f1013,f1380])).
% 0.29/0.39 thf(f1390,definition,(
% 0.29/0.39 spl17_14 <=> (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t @ s3) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ t2 @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ r2) @ (mult_a_ring_ext_a_b @ r @ s2 @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ s2) @ (product_snd_a_a @ x)) @ (mult_a_ring_ext_a_b @ r @ t @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ r3) @ (mult_a_ring_ext_a_b @ r @ s3 @ (product_fst_a_a @ y))))))) = ((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl17_14])],[avatar_definition])).
% 0.29/0.39 thf(f1393,plain,(
% 0.29/0.39 spl17_14),
% 0.29/0.39 inference(avatar_split_clause,[],[f1042,f1390])).
% 0.29/0.39 thf(f1485,definition,(
% 0.29/0.39 spl17_33 <=> (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))) = ((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl17_33])],[avatar_definition])).
% 0.29/0.39 thf(f1489,definition,(
% 0.29/0.39 spl17_34 <=> (((member_a @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))) @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl17_34])],[avatar_definition])).
% 0.29/0.39 thf(f1493,definition,(
% 0.29/0.39 spl17_35 <=> (((member_a @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl17_35])],[avatar_definition])).
% 0.29/0.39 thf(f1495,plain,(
% 0.29/0.39 (((member_a @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (partia1066395285xt_a_b @ r))) != $true) | spl17_35),
% 0.29/0.39 inference(avatar_component_clause,[],[f1493])).
% 0.29/0.39 thf(f1496,plain,(
% 0.29/0.39 spl17_33 | ~spl17_34 | ~spl17_35 | ~spl17_12),
% 0.29/0.39 inference(avatar_split_clause,[],[f1106,f1380,f1493,f1489,f1485])).
% 0.29/0.39 thf(f1565,definition,(
% 0.29/0.39 spl17_49 <=> (((member_a @ t @ (partia1066395285xt_a_b @ r))) = $true)),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl17_49])],[avatar_definition])).
% 0.29/0.39 thf(f1567,plain,(
% 0.29/0.39 (((member_a @ t @ (partia1066395285xt_a_b @ r))) = $true) | ~spl17_49),
% 0.29/0.39 inference(avatar_component_clause,[],[f1565])).
% 0.29/0.39 thf(f1568,plain,(
% 0.29/0.39 spl17_49),
% 0.29/0.39 inference(avatar_split_clause,[],[f1189,f1565])).
% 0.29/0.39 thf(f1629,definition,(
% 0.29/0.39 spl17_62 <=> (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t @ s3) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ t2 @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ r2) @ (mult_a_ring_ext_a_b @ r @ s2 @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ s2) @ (product_snd_a_a @ x)) @ (mult_a_ring_ext_a_b @ r @ t @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ r3) @ (mult_a_ring_ext_a_b @ r @ s3 @ (product_fst_a_a @ y))))))) = ((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))),
% 0.29/0.39 introduced(definition,[new_symbols(definition,[spl17_62])],[avatar_definition])).
% 0.29/0.39 thf(f1632,plain,(
% 0.29/0.39 ~spl17_62),
% 0.29/0.39 inference(avatar_split_clause,[],[f1208,f1629])).
% 0.29/0.39 thf(f1643,plain,(
% 0.29/0.39 spl17_34),
% 0.29/0.39 inference(avatar_split_clause,[],[f1154,f1489])).
% 0.29/0.39 thf(f1701,plain,(
% 0.29/0.39 (((member_a @ t2 @ (partia1066395285xt_a_b @ r))) != $true) | (((member_a @ t @ (partia1066395285xt_a_b @ r))) != $true) | ($true != $true) | spl17_35),
% 0.29/0.39 inference(superposition,[],[f1495,f1162])).
% 0.29/0.39 thf(f1702,plain,(
% 0.29/0.39 (((member_a @ t @ (partia1066395285xt_a_b @ r))) != $true) | (((member_a @ t2 @ (partia1066395285xt_a_b @ r))) != $true) | spl17_35),
% 0.29/0.39 inference(trivial_inequality_removal,[],[f1701])).
% 0.29/0.39 thf(f1703,plain,(
% 0.29/0.39 (((member_a @ t2 @ (partia1066395285xt_a_b @ r))) != $true) | (spl17_35 | ~spl17_49)),
% 0.29/0.39 inference(forward_subsumption_resolution,[],[f1702,f1567])).
% 0.29/0.39 thf(f1704,plain,(
% 0.29/0.39 $false | (~spl17_2 | spl17_35 | ~spl17_49)),
% 0.29/0.39 inference(forward_subsumption_resolution,[],[f1703,f1333])).
% 0.29/0.39 thf(f1705,plain,(
% 0.29/0.39 ~spl17_2 | spl17_35 | ~spl17_49),
% 0.29/0.39 inference(avatar_contradiction_clause,[],[f1704])).
% 0.29/0.39 thf(f1706,definition,(
% 0.29/0.39 (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t @ s3) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ t2 @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ r2) @ (mult_a_ring_ext_a_b @ r @ s2 @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ s2) @ (product_snd_a_a @ x)) @ (mult_a_ring_ext_a_b @ r @ t @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ r3) @ (mult_a_ring_ext_a_b @ r @ s3 @ (product_fst_a_a @ y))))))) != ((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))))))) | (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))) != ((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y)))))))) | (((add_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t @ s3) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ t2 @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ r2) @ (mult_a_ring_ext_a_b @ r @ s2 @ (product_fst_a_a @ x))))) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ s2) @ (product_snd_a_a @ x)) @ (mult_a_ring_ext_a_b @ r @ t @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ r3) @ (mult_a_ring_ext_a_b @ r @ s3 @ (product_fst_a_a @ y))))))) = ((mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ t2 @ t) @ (add_a_b @ r @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s3 @ r2)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ y) @ (product_fst_a_a @ x)))) @ (a_minus_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_snd_a_a @ y)) @ (mult_a_ring_ext_a_b @ r @ s2 @ r3)) @ (mult_a_ring_ext_a_b @ r @ (mult_a_ring_ext_a_b @ r @ s2 @ s3) @ (mult_a_ring_ext_a_b @ r @ (product_snd_a_a @ x) @ (product_fst_a_a @ y))))))))),
% 0.29/0.39 introduced(theory,[theory_tautology_sat_conflict])).
% 0.29/0.39 cnf(s2, plain, spl17_2, inference(sat_conversion,[],[f1334])).
% 0.29/0.39 cnf(s12, plain, spl17_12, inference(sat_conversion,[],[f1383])).
% 0.29/0.39 cnf(s14, plain, spl17_14, inference(sat_conversion,[],[f1393])).
% 0.29/0.39 cnf(s34, plain, ~spl17_12 | spl17_33 | ~spl17_34 | ~spl17_35, inference(sat_conversion,[],[f1496])).
% 0.29/0.39 cnf(s50, plain, spl17_49, inference(sat_conversion,[],[f1568])).
% 0.29/0.39 cnf(s63, plain, ~spl17_62, inference(sat_conversion,[],[f1632])).
% 0.29/0.39 cnf(s66, plain, spl17_34, inference(sat_conversion,[],[f1643])).
% 0.29/0.39 cnf(s79, plain, ~spl17_2 | spl17_35 | ~spl17_49, inference(sat_conversion,[],[f1705])).
% 0.29/0.39 cnf(s80, plain, ~spl17_14 | ~spl17_33 | spl17_62, inference(sat_conversion,[],[f1706])).
% 0.29/0.39 cnf(s87, plain, ~spl17_12 | spl17_33 | ~spl17_35, inference(rat,[],[s34,s66])).
% 0.29/0.39 cnf(s88, plain, ~spl17_33, inference(rat,[],[s80,s63,s14])).
% 0.29/0.39 cnf(s89, plain, ~spl17_35, inference(rat,[],[s87,s88,s12])).
% 0.29/0.39 cnf(s90, plain, ~spl17_2, inference(rat,[],[s79,s50,s89])).
% 0.29/0.39 cnf(s91, plain, $false, inference(rat,[],[s2,s90])).
% 0.29/0.39 thf(f1707,plain,(
% 0.29/0.39 $false),
% 0.29/0.39 inference(avatar_sat_refutation,[],[s91])).
% 0.29/0.39 % SZS output end Proof for theBenchmark
% 0.29/0.39 % (813206)------------------------------
% 0.29/0.39 % (813206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.39 % (813206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.39 % (813206)CaDiCaL version: 2.1.3
% 0.29/0.39 % (813206)Termination reason: Refutation
% 0.29/0.39 % (813206)Time elapsed: 0.041 s
% 0.29/0.39 % (813206)Peak memory usage: 14 MB
% 0.29/0.39 % (813206)Instructions burned: 174 (million)
% 0.29/0.39 % (813198)Success in time 0.09 s
% 0.29/0.39 % Vampire exiting
%------------------------------------------------------------------------------