%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI698_1 : TPTP v9.3.1. Released v6.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:35:06 AM UTC 2026
% Result : Theorem 1.26s 0.54s
% Output : Refutation 1.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ARI698_1 : TPTP v9.3.1. Released v6.3.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.26 % Computer : n001.cluster.edu
% 0.09/0.26 % Model : x86_64 x86_64
% 0.09/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.26 % Memory : 8046.5625MB
% 0.09/0.26 % OS : Linux 6.8.0-71-generic
% 0.09/0.26 % CPULimit : 300
% 0.09/0.26 % WCLimit : 300
% 0.09/0.26 % DateTime : Mon Sep 28 21:03:34 UTC 2026
% 0.09/0.26 % CPUTime :
% 0.09/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.24/0.32 Running first-order model finding
% 0.24/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.26/0.53 % (742912)Will run a generic schedule for satisfiability detection.
% 1.26/0.53 % (742918)% WARNING: option uhcvi not known.
% 1.26/0.53 % (742918)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3971520740:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.26/0.53 % (742917)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1563756477_2999 on theBenchmark for (2999ds/0Mi)
% 1.26/0.53 % (742919)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3453654800:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.26/0.53 % (742921)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2881604653:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.26/0.53 % (742920)dis+10_1_sil=32000:sp=arity:random_seed=312140083:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.26/0.53 % (742917)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.26/0.53 % (742917)Terminated due to inappropriate strategy.
% 1.26/0.53 % (742917)------------------------------
% 1.26/0.53 % (742917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.26/0.53 % (742917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.26/0.53 % (742917)CaDiCaL version: 2.1.3
% 1.26/0.53 % (742917)Termination reason: Inappropriate
% 1.26/0.53 % (742917)Time elapsed: 0.002 s
% 1.26/0.53 % (742917)Peak memory usage: 10 MB
% 1.26/0.53 % (742917)Instructions burned: 2 (million)
% 1.26/0.53 % (742917)------------------------------
% 1.26/0.53 % (742917)------------------------------
% 1.26/0.53 % (742922)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2700212630:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.26/0.53 % (742923)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1760998487:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.26/0.53 % (742930)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3737963708:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.26/0.53 % (742930)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.26/0.53 % (742930)Terminated due to inappropriate strategy.
% 1.26/0.53 % (742930)------------------------------
% 1.26/0.53 % (742930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.26/0.53 % (742930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.26/0.53 % (742930)CaDiCaL version: 2.1.3
% 1.26/0.53 % (742930)Termination reason: Inappropriate
% 1.26/0.53 % (742930)Time elapsed: 0.001 s
% 1.26/0.53 % (742930)Peak memory usage: 10 MB
% 1.26/0.53 % (742930)Instructions burned: 2 (million)
% 1.26/0.53 % (742930)------------------------------
% 1.26/0.53 % (742930)------------------------------
% 1.26/0.53 % (742933)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3782168587:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.26/0.53 % (742920)Instruction limit reached!
% 1.26/0.53 % (742920)------------------------------
% 1.26/0.53 % (742920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.26/0.53 % (742920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.26/0.53 % (742920)CaDiCaL version: 2.1.3
% 1.26/0.53 % (742920)Termination reason: Instruction limit
% 1.26/0.53 % (742920)Termination phase: Saturation
% 1.26/0.54 % (742920)Time elapsed: 0.099 s
% 1.26/0.54 % (742920)Peak memory usage: 13 MB
% 1.26/0.54 % (742920)Instructions burned: 103 (million)
% 1.26/0.54 % (742921)Instruction limit reached!
% 1.26/0.54 % (742921)------------------------------
% 1.26/0.54 % (742921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.26/0.54 % (742921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.26/0.54 % (742921)CaDiCaL version: 2.1.3
% 1.26/0.54 % (742921)Termination reason: Instruction limit
% 1.26/0.54 % (742921)Termination phase: Saturation
% 1.26/0.54 % (742921)Time elapsed: 0.108 s
% 1.26/0.54 % (742921)Peak memory usage: 13 MB
% 1.26/0.54 % (742921)Instructions burned: 117 (million)
% 1.26/0.54 % (742922)Instruction limit reached!
% 1.26/0.54 % (742922)------------------------------
% 1.26/0.54 % (742922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.26/0.54 % (742922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.26/0.54 % (742922)CaDiCaL version: 2.1.3
% 1.26/0.54 % (742922)Termination reason: Instruction limit
% 1.26/0.54 % (742922)Termination phase: Saturation
% 1.26/0.54 % (742922)Time elapsed: 0.125 s
% 1.26/0.54 % (742922)Peak memory usage: 13 MB
% 1.26/0.54 % (742922)Instructions burned: 131 (million)
% 1.26/0.54 % (742935)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2450541111:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.26/0.54 % (742936)ott-21_1_sil=16000:fs=off:random_seed=2736632489:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.26/0.54 % (742937)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2126964236:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.26/0.54 % (742933) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-742912-742933"...
% 1.26/0.54 % (742933)...printing done.
% 1.26/0.54 % (742933)Refutation found. Thanks to Tanya!
% 1.26/0.54 % SZS status Theorem for theBenchmark
% 1.26/0.54 % SZS output start Proof for theBenchmark
% 1.26/0.54 tff(func_def_0, type, n: $int).
% 1.26/0.54 tff(func_def_1, type, x6: $int).
% 1.26/0.54 tff(func_def_2, type, x5: $int).
% 1.26/0.54 tff(func_def_3, type, x4: $int).
% 1.26/0.54 tff(func_def_4, type, x3: $int).
% 1.26/0.54 tff(func_def_5, type, x2: $int).
% 1.26/0.54 tff(func_def_6, type, x1: $int).
% 1.26/0.54 tff(f1,axiom,(
% 1.26/0.54 n = 1000),
% 1.26/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq1)).
% 1.26/0.54 tff(f2,axiom,(
% 1.26/0.54 $sum($sum($sum($sum($sum($product(1,x6),$product(n,x5)),$product(n,x4)),$product(n,x3)),$product(n,x2)),$product(n,x1)) = 0),
% 1.26/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq2)).
% 1.26/0.54 tff(f4,axiom,(
% 1.26/0.54 $difference($difference($difference($difference($sum($product(n,x6),$product(1,x5)),x4),x3),x2),x1) = 0),
% 1.26/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq4)).
% 1.26/0.54 tff(f5,axiom,(
% 1.26/0.54 $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(1,x4)),$product(1,x3)),$product(1,x2)),$product(1,x1)) = 0),
% 1.26/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq5)).
% 1.26/0.54 tff(f7,axiom,(
% 1.26/0.54 $difference($difference($difference($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),x3),x2),x1) = 0),
% 1.26/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq7)).
% 1.26/0.54 tff(f8,axiom,(
% 1.26/0.54 $difference($difference($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(1,x3)),x2),x1) = 0),
% 1.26/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq8)).
% 1.26/0.54 tff(f9,axiom,(
% 1.26/0.54 $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$product(1,x2)),$product(1,x1)) = 0),
% 1.26/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq9)).
% 1.26/0.54 tff(f10,axiom,(
% 1.26/0.54 $sum($difference($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),x2),$product(1,x1)) = 0),
% 1.26/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq10)).
% 1.26/0.54 tff(f11,axiom,(
% 1.26/0.54 $difference($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$product(0,x2)),x1) = 0),
% 1.26/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq11)).
% 1.26/0.54 tff(f12,conjecture,(
% 1.26/0.54 x6 = 0 & x5 = 0 & x4 = 0 & x3 = 0 & x2 = 0 & x1 = 0),
% 1.26/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 1.26/0.54 tff(f13,negated_conjecture,(
% 1.26/0.54 ~(x6 = 0 & x5 = 0 & x4 = 0 & x3 = 0 & x2 = 0 & x1 = 0)),
% 1.26/0.54 inference(negated_conjecture,[status(cth)],[f12])).
% 1.26/0.54 tff(f15,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(n,x6),$product(1,x5)),$uminus(x4)),$uminus(x3)),$uminus(x2)),$uminus(x1))),
% 1.26/0.54 inference(theory_normalization,[],[f4])).
% 1.26/0.54 tff(f17,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$uminus(x3)),$uminus(x2)),$uminus(x1))),
% 1.26/0.54 inference(theory_normalization,[],[f7])).
% 1.26/0.54 tff(f18,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(1,x3)),$uminus(x2)),$uminus(x1))),
% 1.26/0.54 inference(theory_normalization,[],[f8])).
% 1.26/0.54 tff(f19,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$uminus(x2)),$product(1,x1))),
% 1.26/0.54 inference(theory_normalization,[],[f10])).
% 1.26/0.54 tff(f20,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$product(0,x2)),$uminus(x1))),
% 1.26/0.54 inference(theory_normalization,[],[f11])).
% 1.26/0.54 tff(f21,definition,(
% 1.26/0.54 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 1.26/0.54 introduced(theory,[tha_commutativity])).
% 1.26/0.54 tff(f22,definition,(
% 1.26/0.54 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 1.26/0.54 introduced(theory,[tha_associativity])).
% 1.26/0.54 tff(f24,definition,(
% 1.26/0.54 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X0,X1)) = $sum($uminus(X1),$uminus(X0))) )),
% 1.26/0.54 introduced(theory,[tha_inverse_op_op_inverses])).
% 1.26/0.54 tff(f25,definition,(
% 1.26/0.54 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 1.26/0.54 introduced(theory,[tha_inverse_op_unit])).
% 1.26/0.54 tff(f31,definition,(
% 1.26/0.54 ( ! [X0 : $int] : ($uminus($uminus(X0)) = X0) )),
% 1.26/0.54 introduced(theory,[tha_minus_minus_x])).
% 1.26/0.54 tff(f32,definition,(
% 1.26/0.54 ( ! [X0 : $int,X1 : $int] : ($product(X0,X1) = $product(X1,X0)) )),
% 1.26/0.54 introduced(theory,[tha_commutativity])).
% 1.26/0.54 tff(f34,definition,(
% 1.26/0.54 ( ! [X0 : $int] : ($product(X0,1) = X0) )),
% 1.26/0.54 introduced(theory,[tha_right_identity])).
% 1.26/0.54 tff(f35,definition,(
% 1.26/0.54 ( ! [X0 : $int] : (0 = $product(X0,0)) )),
% 1.26/0.54 introduced(theory,[tha_times_zero])).
% 1.26/0.54 tff(f36,definition,(
% 1.26/0.54 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$sum(X1,X2)) = $sum($product(X0,X1),$product(X0,X2))) )),
% 1.26/0.54 introduced(theory,[tha_distributivity])).
% 1.26/0.54 tff(f37,definition,(
% 1.26/0.54 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : (0 = X0 | $product(X0,X2) != X1 | $product(X0,X3) != X1 | X2 = X3) )),
% 1.26/0.54 introduced(theory,[tha_divisibility])).
% 1.26/0.54 tff(f39,plain,(
% 1.26/0.54 x6 != 0 | x5 != 0 | x4 != 0 | x3 != 0 | x2 != 0 | x1 != 0),
% 1.26/0.54 inference(ennf_transformation,[],[f13])).
% 1.26/0.54 tff(f40,plain,(
% 1.26/0.54 n = 1000),
% 1.26/0.54 inference(cnf_transformation,[],[f1])).
% 1.26/0.54 tff(f41,plain,(
% 1.26/0.54 $sum($sum($sum($sum($sum($product(1,x6),$product(n,x5)),$product(n,x4)),$product(n,x3)),$product(n,x2)),$product(n,x1)) = 0),
% 1.26/0.54 inference(cnf_transformation,[],[f2])).
% 1.26/0.54 tff(f43,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(n,x6),$product(1,x5)),$uminus(x4)),$uminus(x3)),$uminus(x2)),$uminus(x1))),
% 1.26/0.54 inference(cnf_transformation,[],[f15])).
% 1.26/0.54 tff(f44,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(1,x4)),$product(1,x3)),$product(1,x2)),$product(1,x1))),
% 1.26/0.54 inference(cnf_transformation,[],[f5])).
% 1.26/0.54 tff(f46,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$uminus(x3)),$uminus(x2)),$uminus(x1))),
% 1.26/0.54 inference(cnf_transformation,[],[f17])).
% 1.26/0.54 tff(f47,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(1,x3)),$uminus(x2)),$uminus(x1))),
% 1.26/0.54 inference(cnf_transformation,[],[f18])).
% 1.26/0.54 tff(f48,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$product(1,x2)),$product(1,x1))),
% 1.26/0.54 inference(cnf_transformation,[],[f9])).
% 1.26/0.54 tff(f49,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$uminus(x2)),$product(1,x1))),
% 1.26/0.54 inference(cnf_transformation,[],[f19])).
% 1.26/0.54 tff(f50,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$product(0,x2)),$uminus(x1))),
% 1.26/0.54 inference(cnf_transformation,[],[f20])).
% 1.26/0.54 tff(f51,plain,(
% 1.26/0.54 x6 != 0 | x5 != 0 | x4 != 0 | x3 != 0 | x2 != 0 | x1 != 0),
% 1.26/0.54 inference(cnf_transformation,[],[f39])).
% 1.26/0.54 tff(f52,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(1,x6),$product(1000,x5)),$product(1000,x4)),$product(1000,x3)),$product(1000,x2)),$product(1000,x1))),
% 1.26/0.54 inference(definition_unfolding,[],[f41,f40,f40,f40,f40,f40])).
% 1.26/0.54 tff(f54,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(1000,x6),$product(1,x5)),$uminus(x4)),$uminus(x3)),$uminus(x2)),$uminus(x1))),
% 1.26/0.54 inference(definition_unfolding,[],[f43,f40])).
% 1.26/0.54 tff(f55,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(1000,x6),$product(0,x5)),$product(1,x4)),$product(1,x3)),$product(1,x2)),$product(1,x1))),
% 1.26/0.54 inference(definition_unfolding,[],[f44,f40])).
% 1.26/0.54 tff(f57,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(1000,x6),$product(0,x5)),$product(0,x4)),$uminus(x3)),$uminus(x2)),$uminus(x1))),
% 1.26/0.54 inference(definition_unfolding,[],[f46,f40])).
% 1.26/0.54 tff(f58,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(1000,x6),$product(0,x5)),$product(0,x4)),$product(1,x3)),$uminus(x2)),$uminus(x1))),
% 1.26/0.54 inference(definition_unfolding,[],[f47,f40])).
% 1.26/0.54 tff(f59,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(1000,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$product(1,x2)),$product(1,x1))),
% 1.26/0.54 inference(definition_unfolding,[],[f48,f40])).
% 1.26/0.54 tff(f60,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(1000,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$uminus(x2)),$product(1,x1))),
% 1.26/0.54 inference(definition_unfolding,[],[f49,f40])).
% 1.26/0.54 tff(f61,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(1000,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$product(0,x2)),$uminus(x1))),
% 1.26/0.54 inference(definition_unfolding,[],[f50,f40])).
% 1.26/0.54 tff(f62,plain,(
% 1.26/0.54 ( ! [X2 : $int,X3 : $int,X0 : $int] : ($product(X0,X2) != $product(X0,X3) | 0 = X0 | X2 = X3) )),
% 1.26/0.54 inference(equality_resolution,[],[f37])).
% 1.26/0.54 tff(f63,plain,(
% 1.26/0.54 0 = $sum($product(1000,x6),$uminus(x1))),
% 1.26/0.54 inference(evaluation,[],[f61])).
% 1.26/0.54 tff(f64,plain,(
% 1.26/0.54 0 = $sum($sum($product(1000,x6),$uminus(x2)),x1)),
% 1.26/0.54 inference(evaluation,[],[f60])).
% 1.26/0.54 tff(f65,plain,(
% 1.26/0.54 0 = $sum($sum($product(1000,x6),x2),x1)),
% 1.26/0.54 inference(evaluation,[],[f59])).
% 1.26/0.54 tff(f66,plain,(
% 1.26/0.54 0 = $sum($sum($sum($product(1000,x6),x3),$uminus(x2)),$uminus(x1))),
% 1.26/0.54 inference(evaluation,[],[f58])).
% 1.26/0.54 tff(f67,plain,(
% 1.26/0.54 0 = $sum($sum($sum($product(1000,x6),$uminus(x3)),$uminus(x2)),$uminus(x1))),
% 1.26/0.54 inference(evaluation,[],[f57])).
% 1.26/0.54 tff(f69,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($product(1000,x6),x4),x3),x2),x1)),
% 1.26/0.54 inference(evaluation,[],[f55])).
% 1.26/0.54 tff(f70,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum($product(1000,x6),x5),$uminus(x4)),$uminus(x3)),$uminus(x2)),$uminus(x1))),
% 1.26/0.54 inference(evaluation,[],[f54])).
% 1.26/0.54 tff(f71,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($sum(x6,$product(1000,x5)),$product(1000,x4)),$product(1000,x3)),$product(1000,x2)),$product(1000,x1))),
% 1.26/0.54 inference(evaluation,[],[f52])).
% 1.26/0.54 tff(f73,definition,(
% 1.26/0.54 spl0_1 <=> x1 = 0),
% 1.26/0.54 introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition])).
% 1.26/0.54 tff(f74,plain,(
% 1.26/0.54 x1 = 0 | ~spl0_1),
% 1.26/0.54 inference(avatar_component_clause,[],[f73])).
% 1.26/0.54 tff(f75,plain,(
% 1.26/0.54 x1 != 0 | spl0_1),
% 1.26/0.54 inference(avatar_component_clause,[],[f73])).
% 1.26/0.54 tff(f77,definition,(
% 1.26/0.54 spl0_2 <=> x2 = 0),
% 1.26/0.54 introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition])).
% 1.26/0.54 tff(f81,definition,(
% 1.26/0.54 spl0_3 <=> x3 = 0),
% 1.26/0.54 introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition])).
% 1.26/0.54 tff(f85,definition,(
% 1.26/0.54 spl0_4 <=> x4 = 0),
% 1.26/0.54 introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition])).
% 1.26/0.54 tff(f89,definition,(
% 1.26/0.54 spl0_5 <=> x5 = 0),
% 1.26/0.54 introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition])).
% 1.26/0.54 tff(f90,plain,(
% 1.26/0.54 x5 = 0 | ~spl0_5),
% 1.26/0.54 inference(avatar_component_clause,[],[f89])).
% 1.26/0.54 tff(f93,definition,(
% 1.26/0.54 spl0_6 <=> x6 = 0),
% 1.26/0.54 introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition])).
% 1.26/0.54 tff(f95,plain,(
% 1.26/0.54 x6 != 0 | spl0_6),
% 1.26/0.54 inference(avatar_component_clause,[],[f93])).
% 1.26/0.54 tff(f96,plain,(
% 1.26/0.54 ~spl0_1 | ~spl0_2 | ~spl0_3 | ~spl0_4 | ~spl0_5 | ~spl0_6),
% 1.26/0.54 inference(avatar_split_clause,[],[f51,f93,f89,f85,f81,f77,f73])).
% 1.26/0.54 tff(f98,plain,(
% 1.26/0.54 0 = $sum($sum($sum($product(1000,x6),$sum(x4,x3)),x2),x1)),
% 1.26/0.54 inference(backward_demodulation,[],[f69,f22])).
% 1.26/0.54 tff(f99,plain,(
% 1.26/0.54 0 = $sum($product(1000,x6),$sum($uminus(x2),x1))),
% 1.26/0.54 inference(backward_demodulation,[],[f64,f22])).
% 1.26/0.54 tff(f100,plain,(
% 1.26/0.54 0 = $sum($product(1000,x6),$sum(x2,x1))),
% 1.26/0.54 inference(backward_demodulation,[],[f65,f22])).
% 1.26/0.54 tff(f101,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum(x6,$product(1000,x5)),$product(1000,x4)),$product(1000,x3)),$sum($product(1000,x2),$product(1000,x1)))),
% 1.26/0.54 inference(backward_demodulation,[],[f71,f22])).
% 1.26/0.54 tff(f102,plain,(
% 1.26/0.54 0 = $sum($sum($product(1000,x6),x3),$sum($uminus(x2),$uminus(x1)))),
% 1.26/0.54 inference(backward_demodulation,[],[f66,f22])).
% 1.26/0.54 tff(f103,plain,(
% 1.26/0.54 0 = $sum($sum($product(1000,x6),$uminus(x3)),$sum($uminus(x2),$uminus(x1)))),
% 1.26/0.54 inference(backward_demodulation,[],[f67,f22])).
% 1.26/0.54 tff(f104,plain,(
% 1.26/0.54 0 = $sum($sum($sum($sum($product(1000,x6),x5),$uminus(x4)),$uminus(x3)),$sum($uminus(x2),$uminus(x1)))),
% 1.26/0.54 inference(backward_demodulation,[],[f70,f22])).
% 1.26/0.54 tff(f107,plain,(
% 1.26/0.54 0 = $sum($sum($uminus(x2),$uminus(x1)),$sum($sum($sum($product(1000,x6),x5),$uminus(x4)),$uminus(x3)))),
% 1.26/0.54 inference(forward_demodulation,[],[f104,f21])).
% 1.26/0.54 tff(f108,plain,(
% 1.26/0.54 0 = $sum($sum($uminus(x2),$uminus(x1)),$sum($product(1000,x6),$uminus(x3)))),
% 1.26/0.54 inference(forward_demodulation,[],[f103,f21])).
% 1.26/0.54 tff(f109,plain,(
% 1.26/0.54 0 = $sum($sum($uminus(x2),$uminus(x1)),$sum($product(1000,x6),x3))),
% 1.26/0.54 inference(forward_demodulation,[],[f102,f21])).
% 1.26/0.54 tff(f110,plain,(
% 1.26/0.54 0 = $sum($sum($product(1000,x2),$product(1000,x1)),$sum($sum($sum(x6,$product(1000,x5)),$product(1000,x4)),$product(1000,x3)))),
% 1.26/0.54 inference(forward_demodulation,[],[f101,f21])).
% 1.26/0.54 tff(f111,plain,(
% 1.26/0.54 0 = $sum($product(1000,x6),$sum(x1,$uminus(x2)))),
% 1.26/0.54 inference(forward_demodulation,[],[f99,f21])).
% 1.26/0.54 tff(f112,plain,(
% 1.26/0.54 0 = $sum(x1,$sum($sum($product(1000,x6),$sum(x4,x3)),x2))),
% 1.26/0.54 inference(forward_demodulation,[],[f98,f21])).
% 1.26/0.54 tff(f115,plain,(
% 1.26/0.54 0 = $sum($uminus(x2),$sum($uminus(x1),$sum($sum($sum($product(1000,x6),x5),$uminus(x4)),$uminus(x3))))),
% 1.26/0.54 inference(forward_demodulation,[],[f107,f22])).
% 1.26/0.54 tff(f116,plain,(
% 1.26/0.54 0 = $sum($uminus(x2),$sum($uminus(x1),$sum($product(1000,x6),$uminus(x3))))),
% 1.26/0.54 inference(forward_demodulation,[],[f108,f22])).
% 1.26/0.54 tff(f117,plain,(
% 1.26/0.54 0 = $sum($uminus(x2),$sum($uminus(x1),$sum($product(1000,x6),x3)))),
% 1.26/0.54 inference(forward_demodulation,[],[f109,f22])).
% 1.26/0.54 tff(f118,plain,(
% 1.26/0.54 0 = $sum($product(1000,x2),$sum($product(1000,x1),$sum($sum($sum(x6,$product(1000,x5)),$product(1000,x4)),$product(1000,x3))))),
% 1.26/0.54 inference(forward_demodulation,[],[f110,f22])).
% 1.26/0.54 tff(f119,plain,(
% 1.26/0.54 0 = $sum(x1,$sum(x2,$sum($product(1000,x6),$sum(x4,x3))))),
% 1.26/0.54 inference(forward_demodulation,[],[f112,f21])).
% 1.26/0.54 tff(f122,plain,(
% 1.26/0.54 0 = $sum($uminus(x2),$sum($uminus(x1),$sum($uminus(x3),$sum($sum($product(1000,x6),x5),$uminus(x4)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f115,f21])).
% 1.26/0.54 tff(f123,plain,(
% 1.26/0.54 0 = $sum($uminus(x2),$sum($uminus(x1),$sum($uminus(x3),$product(1000,x6))))),
% 1.26/0.54 inference(forward_demodulation,[],[f116,f21])).
% 1.26/0.54 tff(f124,plain,(
% 1.26/0.54 0 = $sum($uminus(x2),$sum($uminus(x1),$sum(x3,$product(1000,x6))))),
% 1.26/0.54 inference(forward_demodulation,[],[f117,f21])).
% 1.26/0.54 tff(f125,plain,(
% 1.26/0.54 0 = $sum($product(1000,x2),$sum($product(1000,x1),$sum($product(1000,x3),$sum($sum(x6,$product(1000,x5)),$product(1000,x4)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f118,f21])).
% 1.26/0.54 tff(f128,plain,(
% 1.26/0.54 0 = $sum($uminus(x2),$sum($uminus(x1),$sum($uminus(x3),$sum($uminus(x4),$sum($product(1000,x6),x5)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f122,f21])).
% 1.26/0.54 tff(f129,plain,(
% 1.26/0.54 0 = $sum($product(1000,x2),$sum($product(1000,x1),$sum($product(1000,x3),$sum($product(1000,x4),$sum(x6,$product(1000,x5))))))),
% 1.26/0.54 inference(forward_demodulation,[],[f125,f21])).
% 1.26/0.54 tff(f131,plain,(
% 1.26/0.54 0 = $sum($uminus(x2),$sum($uminus(x1),$sum($uminus(x3),$sum($uminus(x4),$sum(x5,$product(1000,x6))))))),
% 1.26/0.54 inference(forward_demodulation,[],[f128,f21])).
% 1.26/0.54 tff(f161,plain,(
% 1.26/0.54 0 = $sum($uminus(x1),$product(1000,x6))),
% 1.26/0.54 inference(superposition,[],[f21,f63])).
% 1.26/0.54 tff(f256,plain,(
% 1.26/0.54 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 1.26/0.54 inference(superposition,[],[f22,f25])).
% 1.26/0.54 tff(f260,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(0,X0) = $sum($product(1000,x6),$sum($sum(x2,x1),X0))) )),
% 1.26/0.54 inference(superposition,[],[f22,f100])).
% 1.26/0.54 tff(f263,plain,(
% 1.26/0.54 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum($uminus(X1),$sum($uminus(X0),X2)) = $sum($uminus($sum(X0,X1)),X2)) )),
% 1.26/0.54 inference(superposition,[],[f22,f24])).
% 1.26/0.54 tff(f270,plain,(
% 1.26/0.54 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum(X2,$sum(X0,X1))) )),
% 1.26/0.54 inference(superposition,[],[f21,f22])).
% 1.26/0.54 tff(f278,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum($product(1000,x6),$sum($sum(x2,x1),X0)) = X0) )),
% 1.26/0.54 inference(evaluation,[],[f260])).
% 1.26/0.54 tff(f280,plain,(
% 1.26/0.54 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 1.26/0.54 inference(evaluation,[],[f256])).
% 1.26/0.54 tff(f282,plain,(
% 1.26/0.54 0 = $sum($uminus(x2),$sum($uminus(x1),$sum($uminus($sum(x4,x3)),$sum(x5,$product(1000,x6)))))),
% 1.26/0.54 inference(backward_demodulation,[],[f131,f263])).
% 1.26/0.54 tff(f283,plain,(
% 1.26/0.54 0 = $sum($uminus($sum(x1,x2)),$sum($uminus(x3),$product(1000,x6)))),
% 1.26/0.54 inference(backward_demodulation,[],[f123,f263])).
% 1.26/0.54 tff(f284,plain,(
% 1.26/0.54 0 = $sum($uminus($sum(x1,x2)),$sum(x3,$product(1000,x6)))),
% 1.26/0.54 inference(backward_demodulation,[],[f124,f263])).
% 1.26/0.54 tff(f287,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum($product(1000,x6),$sum(x2,$sum(x1,X0))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f278,f22])).
% 1.26/0.54 tff(f289,plain,(
% 1.26/0.54 0 = $sum($product(1000,x6),$sum($uminus($sum(x1,x2)),x3))),
% 1.26/0.54 inference(forward_demodulation,[],[f284,f270])).
% 1.26/0.54 tff(f290,plain,(
% 1.26/0.54 0 = $sum($product(1000,x6),$sum($uminus($sum(x1,x2)),$uminus(x3)))),
% 1.26/0.54 inference(forward_demodulation,[],[f283,f270])).
% 1.26/0.54 tff(f291,plain,(
% 1.26/0.54 0 = $sum($uminus($sum(x1,x2)),$sum($uminus($sum(x4,x3)),$sum(x5,$product(1000,x6))))),
% 1.26/0.54 inference(forward_demodulation,[],[f282,f263])).
% 1.26/0.54 tff(f295,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x2,$sum($sum(x1,X0),$product(1000,x6))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f287,f270])).
% 1.26/0.54 tff(f296,plain,(
% 1.26/0.54 0 = $sum(x3,$sum($product(1000,x6),$uminus($sum(x1,x2))))),
% 1.26/0.54 inference(forward_demodulation,[],[f289,f270])).
% 1.26/0.54 tff(f297,plain,(
% 1.26/0.54 0 = $sum($uminus(x3),$sum($product(1000,x6),$uminus($sum(x1,x2))))),
% 1.26/0.54 inference(forward_demodulation,[],[f290,f270])).
% 1.26/0.54 tff(f298,plain,(
% 1.26/0.54 0 = $sum($uminus($sum(x4,x3)),$sum($sum(x5,$product(1000,x6)),$uminus($sum(x1,x2))))),
% 1.26/0.54 inference(forward_demodulation,[],[f291,f270])).
% 1.26/0.54 tff(f301,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x2,$sum($product(1000,x6),$sum(x1,X0))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f295,f21])).
% 1.26/0.54 tff(f302,plain,(
% 1.26/0.54 0 = $sum(x3,$sum($product(1000,x6),$uminus($sum(x2,x1))))),
% 1.26/0.54 inference(forward_demodulation,[],[f296,f21])).
% 1.26/0.54 tff(f303,plain,(
% 1.26/0.54 0 = $sum($uminus(x3),$sum($product(1000,x6),$uminus($sum(x2,x1))))),
% 1.26/0.54 inference(forward_demodulation,[],[f297,f21])).
% 1.26/0.54 tff(f304,plain,(
% 1.26/0.54 0 = $sum($uminus($sum(x4,x3)),$sum($uminus($sum(x1,x2)),$sum(x5,$product(1000,x6))))),
% 1.26/0.54 inference(forward_demodulation,[],[f298,f21])).
% 1.26/0.54 tff(f307,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x2,$sum(x1,$sum(X0,$product(1000,x6)))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f301,f270])).
% 1.26/0.54 tff(f308,plain,(
% 1.26/0.54 0 = $sum($uminus($sum($sum(x1,x2),$sum(x4,x3))),$sum(x5,$product(1000,x6)))),
% 1.26/0.54 inference(forward_demodulation,[],[f304,f263])).
% 1.26/0.54 tff(f310,plain,(
% 1.26/0.54 0 = $sum($sum(x5,$product(1000,x6)),$uminus($sum($sum(x1,x2),$sum(x4,x3))))),
% 1.26/0.54 inference(forward_demodulation,[],[f308,f21])).
% 1.26/0.54 tff(f312,plain,(
% 1.26/0.54 0 = $sum(x5,$sum($product(1000,x6),$uminus($sum($sum(x1,x2),$sum(x4,x3)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f310,f22])).
% 1.26/0.54 tff(f314,plain,(
% 1.26/0.54 0 = $sum(x5,$sum($product(1000,x6),$uminus($sum($sum(x4,x3),$sum(x1,x2)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f312,f21])).
% 1.26/0.54 tff(f316,plain,(
% 1.26/0.54 0 = $sum(x5,$sum($product(1000,x6),$uminus($sum(x2,$sum($sum(x4,x3),x1)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f314,f270])).
% 1.26/0.54 tff(f318,plain,(
% 1.26/0.54 0 = $sum(x5,$sum($product(1000,x6),$uminus($sum(x2,$sum(x1,$sum(x4,x3))))))),
% 1.26/0.54 inference(forward_demodulation,[],[f316,f21])).
% 1.26/0.54 tff(f320,plain,(
% 1.26/0.54 0 = $sum(x5,$sum($product(1000,x6),$uminus($sum(x2,$sum(x3,$sum(x1,x4))))))),
% 1.26/0.54 inference(forward_demodulation,[],[f318,f270])).
% 1.26/0.54 tff(f322,plain,(
% 1.26/0.54 0 = $sum(x5,$sum($product(1000,x6),$uminus($sum(x3,$sum($sum(x1,x4),x2)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f320,f270])).
% 1.26/0.54 tff(f324,plain,(
% 1.26/0.54 0 = $sum(x5,$sum($product(1000,x6),$uminus($sum(x3,$sum(x2,$sum(x1,x4))))))),
% 1.26/0.54 inference(forward_demodulation,[],[f322,f21])).
% 1.26/0.54 tff(f326,plain,(
% 1.26/0.54 0 = $sum(x5,$sum($product(1000,x6),$uminus($sum(x3,$sum(x4,$sum(x2,x1))))))),
% 1.26/0.54 inference(forward_demodulation,[],[f324,f270])).
% 1.26/0.54 tff(f328,plain,(
% 1.26/0.54 0 = $sum(x5,$sum($product(1000,x6),$uminus($sum(x4,$sum($sum(x2,x1),x3)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f326,f270])).
% 1.26/0.54 tff(f330,plain,(
% 1.26/0.54 0 = $sum(x5,$sum($product(1000,x6),$uminus($sum(x4,$sum(x3,$sum(x2,x1))))))),
% 1.26/0.54 inference(forward_demodulation,[],[f328,f21])).
% 1.26/0.54 tff(f385,plain,(
% 1.26/0.54 ( ! [X0 : $int,X1 : $int] : ($product(X0,$sum(1,X1)) = $sum(X0,$product(X0,X1))) )),
% 1.26/0.54 inference(superposition,[],[f36,f34])).
% 1.26/0.54 tff(f397,plain,(
% 1.26/0.54 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : ($sum($product(X0,X1),$sum($product(X0,X2),X3)) = $sum($product(X0,$sum(X1,X2)),X3)) )),
% 1.26/0.54 inference(superposition,[],[f22,f36])).
% 1.26/0.54 tff(f400,plain,(
% 1.26/0.54 0 = $sum($product(1000,x2),$sum($product(1000,x1),$sum($product(1000,$sum(x3,x4)),$sum(x6,$product(1000,x5)))))),
% 1.26/0.54 inference(backward_demodulation,[],[f129,f397])).
% 1.26/0.54 tff(f404,plain,(
% 1.26/0.54 0 = $sum($product(1000,$sum(x2,x1)),$sum($product(1000,$sum(x3,x4)),$sum(x6,$product(1000,x5))))),
% 1.26/0.54 inference(forward_demodulation,[],[f400,f397])).
% 1.26/0.54 tff(f407,plain,(
% 1.26/0.54 0 = $sum($product(1000,$sum($sum(x2,x1),$sum(x3,x4))),$sum(x6,$product(1000,x5)))),
% 1.26/0.54 inference(forward_demodulation,[],[f404,f397])).
% 1.26/0.54 tff(f410,plain,(
% 1.26/0.54 0 = $sum($sum(x6,$product(1000,x5)),$product(1000,$sum($sum(x2,x1),$sum(x3,x4))))),
% 1.26/0.54 inference(forward_demodulation,[],[f407,f21])).
% 1.26/0.54 tff(f411,plain,(
% 1.26/0.54 0 = $sum(x6,$sum($product(1000,x5),$product(1000,$sum($sum(x2,x1),$sum(x3,x4)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f410,f22])).
% 1.26/0.54 tff(f412,plain,(
% 1.26/0.54 0 = $sum(x6,$product(1000,$sum(x5,$sum($sum(x2,x1),$sum(x3,x4)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f411,f36])).
% 1.26/0.54 tff(f413,plain,(
% 1.26/0.54 0 = $sum(x6,$product(1000,$sum(x5,$sum($sum(x3,x4),$sum(x2,x1)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f412,f21])).
% 1.26/0.54 tff(f414,plain,(
% 1.26/0.54 0 = $sum(x6,$product(1000,$sum(x5,$sum(x1,$sum($sum(x3,x4),x2)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f413,f270])).
% 1.26/0.54 tff(f415,plain,(
% 1.26/0.54 0 = $sum(x6,$product(1000,$sum(x5,$sum(x2,$sum(x1,$sum(x3,x4))))))),
% 1.26/0.54 inference(forward_demodulation,[],[f414,f270])).
% 1.26/0.54 tff(f416,plain,(
% 1.26/0.54 0 = $sum(x6,$product(1000,$sum(x5,$sum(x2,$sum(x4,$sum(x1,x3))))))),
% 1.26/0.54 inference(forward_demodulation,[],[f415,f270])).
% 1.26/0.54 tff(f417,plain,(
% 1.26/0.54 0 = $sum(x6,$product(1000,$sum(x5,$sum(x4,$sum($sum(x1,x3),x2)))))),
% 1.26/0.54 inference(forward_demodulation,[],[f416,f270])).
% 1.26/0.54 tff(f418,plain,(
% 1.26/0.54 0 = $sum(x6,$product(1000,$sum(x5,$sum(x4,$sum(x2,$sum(x1,x3))))))),
% 1.26/0.54 inference(forward_demodulation,[],[f417,f21])).
% 1.26/0.54 tff(f419,plain,(
% 1.26/0.54 0 = $sum(x6,$product(1000,$sum(x5,$sum(x4,$sum(x3,$sum(x2,x1))))))),
% 1.26/0.54 inference(forward_demodulation,[],[f418,f270])).
% 1.26/0.54 tff(f452,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(0,X0) = $sum(x1,$sum($sum(x2,$sum($product(1000,x6),$sum(x4,x3))),X0))) )),
% 1.26/0.54 inference(superposition,[],[f22,f119])).
% 1.26/0.54 tff(f453,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x1,$sum($sum(x2,$sum($product(1000,x6),$sum(x4,x3))),X0)) = X0) )),
% 1.26/0.54 inference(evaluation,[],[f452])).
% 1.26/0.54 tff(f454,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x1,$sum(x2,$sum($sum($product(1000,x6),$sum(x4,x3)),X0))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f453,f22])).
% 1.26/0.54 tff(f455,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x2,$sum($sum($sum($product(1000,x6),$sum(x4,x3)),X0),x1)) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f454,f270])).
% 1.26/0.54 tff(f456,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x2,$sum($sum($product(1000,x6),$sum(x4,x3)),$sum(X0,x1))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f455,f22])).
% 1.26/0.54 tff(f457,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x2,$sum($product(1000,x6),$sum($sum(x4,x3),$sum(X0,x1)))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f456,f22])).
% 1.26/0.54 tff(f458,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x2,$sum($product(1000,x6),$sum(x4,$sum(x3,$sum(X0,x1))))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f457,f22])).
% 1.26/0.54 tff(f459,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x2,$sum(x4,$sum($sum(x3,$sum(X0,x1)),$product(1000,x6)))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f458,f270])).
% 1.26/0.54 tff(f460,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x4,$sum($sum($sum(x3,$sum(X0,x1)),$product(1000,x6)),x2)) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f459,f270])).
% 1.26/0.54 tff(f461,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x4,$sum($sum(x3,$sum(X0,x1)),$sum($product(1000,x6),x2))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f460,f22])).
% 1.26/0.54 tff(f462,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x4,$sum(x3,$sum($sum(X0,x1),$sum($product(1000,x6),x2)))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f461,f22])).
% 1.26/0.54 tff(f463,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x4,$sum(x3,$sum(X0,$sum(x1,$sum($product(1000,x6),x2))))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f462,f22])).
% 1.26/0.54 tff(f464,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x4,$sum(x3,$sum(X0,$sum(x2,$sum(x1,$product(1000,x6)))))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f463,f270])).
% 1.26/0.54 tff(f513,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(0,X0) = $sum(x6,$sum($product(1000,$sum(x5,$sum(x4,$sum(x3,$sum(x2,x1))))),X0))) )),
% 1.26/0.54 inference(superposition,[],[f22,f419])).
% 1.26/0.54 tff(f514,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x6,$sum($product(1000,$sum(x5,$sum(x4,$sum(x3,$sum(x2,x1))))),X0)) = X0) )),
% 1.26/0.54 inference(evaluation,[],[f513])).
% 1.26/0.54 tff(f523,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(0,X0) = $sum(x5,$sum($sum($product(1000,x6),$uminus($sum(x4,$sum(x3,$sum(x2,x1))))),X0))) )),
% 1.26/0.54 inference(superposition,[],[f22,f330])).
% 1.26/0.54 tff(f524,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x5,$sum($sum($product(1000,x6),$uminus($sum(x4,$sum(x3,$sum(x2,x1))))),X0)) = X0) )),
% 1.26/0.54 inference(evaluation,[],[f523])).
% 1.26/0.54 tff(f525,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x5,$sum($product(1000,x6),$sum($uminus($sum(x4,$sum(x3,$sum(x2,x1)))),X0))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f524,f22])).
% 1.26/0.54 tff(f552,plain,(
% 1.26/0.54 ( ! [X0 : $int,X1 : $int] : ($uminus(X0) = $sum(X1,$uminus($sum(X0,X1)))) )),
% 1.26/0.54 inference(superposition,[],[f280,f24])).
% 1.26/0.54 tff(f553,plain,(
% 1.26/0.54 $product(1000,x6) = $sum(x1,0)),
% 1.26/0.54 inference(superposition,[],[f280,f161])).
% 1.26/0.54 tff(f554,plain,(
% 1.26/0.54 $sum($product(1000,x6),$uminus($sum(x2,x1))) = $sum(x3,0)),
% 1.26/0.54 inference(superposition,[],[f280,f303])).
% 1.26/0.54 tff(f569,plain,(
% 1.26/0.54 x3 = $sum($product(1000,x6),$uminus($sum(x2,x1)))),
% 1.26/0.54 inference(evaluation,[],[f554])).
% 1.26/0.54 tff(f570,plain,(
% 1.26/0.54 x1 = $product(1000,x6)),
% 1.26/0.54 inference(evaluation,[],[f553])).
% 1.26/0.54 tff(f574,plain,(
% 1.26/0.54 0 = $sum(x3,x3)),
% 1.26/0.54 inference(backward_demodulation,[],[f302,f569])).
% 1.26/0.54 tff(f576,plain,(
% 1.26/0.54 0 = $sum(x1,$sum(x2,x1))),
% 1.26/0.54 inference(backward_demodulation,[],[f100,f570])).
% 1.26/0.54 tff(f577,plain,(
% 1.26/0.54 0 = $sum(x1,$sum(x1,$uminus(x2)))),
% 1.26/0.54 inference(backward_demodulation,[],[f111,f570])).
% 1.26/0.54 tff(f578,plain,(
% 1.26/0.54 0 = $sum(x1,$sum(x2,$sum(x1,$sum(x4,x3))))),
% 1.26/0.54 inference(backward_demodulation,[],[f119,f570])).
% 1.26/0.54 tff(f584,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x2,$sum(x1,$sum(X0,x1))) = X0) )),
% 1.26/0.54 inference(backward_demodulation,[],[f307,f570])).
% 1.26/0.54 tff(f585,plain,(
% 1.26/0.54 0 = $sum(x5,$sum(x1,$uminus($sum(x4,$sum(x3,$sum(x2,x1))))))),
% 1.26/0.54 inference(backward_demodulation,[],[f330,f570])).
% 1.26/0.54 tff(f588,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x4,$sum(x3,$sum(X0,$sum(x2,$sum(x1,x1))))) = X0) )),
% 1.26/0.54 inference(backward_demodulation,[],[f464,f570])).
% 1.26/0.54 tff(f591,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x5,$sum(x1,$sum($uminus($sum(x4,$sum(x3,$sum(x2,x1)))),X0))) = X0) )),
% 1.26/0.54 inference(backward_demodulation,[],[f525,f570])).
% 1.26/0.54 tff(f593,plain,(
% 1.26/0.54 x3 = $sum(x1,$uminus($sum(x2,x1)))),
% 1.26/0.54 inference(backward_demodulation,[],[f569,f570])).
% 1.26/0.54 tff(f598,plain,(
% 1.26/0.54 x3 = $uminus(x2)),
% 1.26/0.54 inference(forward_demodulation,[],[f593,f552])).
% 1.26/0.54 tff(f605,plain,(
% 1.26/0.54 0 = $sum(x2,$sum($sum(x1,$sum(x4,x3)),x1))),
% 1.26/0.54 inference(forward_demodulation,[],[f578,f270])).
% 1.26/0.54 tff(f606,plain,(
% 1.26/0.54 0 = $sum(x2,$sum(x1,x1))),
% 1.26/0.54 inference(forward_demodulation,[],[f576,f270])).
% 1.26/0.54 tff(f607,plain,(
% 1.26/0.54 0 = $sum(x1,$sum(x1,x3))),
% 1.26/0.54 inference(backward_demodulation,[],[f577,f598])).
% 1.26/0.54 tff(f611,plain,(
% 1.26/0.54 0 = $sum(x2,$sum(x1,$sum($sum(x4,x3),x1)))),
% 1.26/0.54 inference(forward_demodulation,[],[f605,f22])).
% 1.26/0.54 tff(f612,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x4,$sum(x3,$sum(X0,0))) = X0) )),
% 1.26/0.54 inference(backward_demodulation,[],[f588,f606])).
% 1.26/0.54 tff(f615,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x4,$sum(x3,X0)) = X0) )),
% 1.26/0.54 inference(evaluation,[],[f612])).
% 1.26/0.54 tff(f616,plain,(
% 1.26/0.54 0 = $sum(x3,$sum(x1,x1))),
% 1.26/0.54 inference(forward_demodulation,[],[f607,f270])).
% 1.26/0.54 tff(f620,plain,(
% 1.26/0.54 0 = $sum(x4,x3)),
% 1.26/0.54 inference(forward_demodulation,[],[f611,f584])).
% 1.26/0.54 tff(f621,plain,(
% 1.26/0.54 0 = $sum(x5,$sum(x1,$uminus($sum(x2,x1))))),
% 1.26/0.54 inference(backward_demodulation,[],[f585,f615])).
% 1.26/0.54 tff(f623,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x5,$sum(x1,$sum($uminus($sum(x2,x1)),X0))) = X0) )),
% 1.26/0.54 inference(backward_demodulation,[],[f591,f615])).
% 1.26/0.54 tff(f625,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x6,$sum($product(1000,$sum(x5,$sum(x2,x1))),X0)) = X0) )),
% 1.26/0.54 inference(backward_demodulation,[],[f514,f615])).
% 1.26/0.54 tff(f629,plain,(
% 1.26/0.54 0 = $sum(x5,$uminus(x2))),
% 1.26/0.54 inference(forward_demodulation,[],[f621,f552])).
% 1.26/0.54 tff(f632,plain,(
% 1.26/0.54 0 = $sum(x5,x3)),
% 1.26/0.54 inference(forward_demodulation,[],[f629,f598])).
% 1.26/0.54 tff(f635,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($uminus($sum(x2,X0)) = $sum($uminus(X0),x3)) )),
% 1.26/0.54 inference(superposition,[],[f24,f598])).
% 1.26/0.54 tff(f637,plain,(
% 1.26/0.54 0 = $sum(x2,x3)),
% 1.26/0.54 inference(superposition,[],[f25,f598])).
% 1.26/0.54 tff(f639,plain,(
% 1.26/0.54 0 = $sum(x3,x2)),
% 1.26/0.54 inference(forward_demodulation,[],[f637,f21])).
% 1.26/0.54 tff(f640,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($uminus($sum(x2,X0)) = $sum(x3,$uminus(X0))) )),
% 1.26/0.54 inference(forward_demodulation,[],[f635,f21])).
% 1.26/0.54 tff(f642,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x5,$sum(x1,$sum($sum(x3,$uminus(x1)),X0))) = X0) )),
% 1.26/0.54 inference(backward_demodulation,[],[f623,f640])).
% 1.26/0.54 tff(f645,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x5,$sum(x1,$sum(x3,$sum($uminus(x1),X0)))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f642,f22])).
% 1.26/0.54 tff(f647,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x5,$sum(x3,$sum($sum($uminus(x1),X0),x1))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f645,f270])).
% 1.26/0.54 tff(f649,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x5,$sum(x3,$sum($uminus(x1),$sum(X0,x1)))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f647,f22])).
% 1.26/0.54 tff(f651,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x5,$sum(x3,$sum(x1,$sum($uminus(x1),X0)))) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f649,f270])).
% 1.26/0.54 tff(f653,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x5,$sum(x3,X0)) = X0) )),
% 1.26/0.54 inference(forward_demodulation,[],[f651,f280])).
% 1.26/0.54 tff(f734,plain,(
% 1.26/0.54 x3 = $sum(x4,0)),
% 1.26/0.54 inference(superposition,[],[f615,f574])).
% 1.26/0.54 tff(f735,plain,(
% 1.26/0.54 x2 = $sum(x4,0)),
% 1.26/0.54 inference(superposition,[],[f615,f639])).
% 1.26/0.54 tff(f736,plain,(
% 1.26/0.54 $sum(x1,x1) = $sum(x4,0)),
% 1.26/0.54 inference(superposition,[],[f615,f616])).
% 1.26/0.54 tff(f746,plain,(
% 1.26/0.54 x4 = $sum(x1,x1)),
% 1.26/0.54 inference(evaluation,[],[f736])).
% 1.26/0.54 tff(f747,plain,(
% 1.26/0.54 x4 = x2),
% 1.26/0.54 inference(evaluation,[],[f735])).
% 1.26/0.54 tff(f748,plain,(
% 1.26/0.54 x4 = x3),
% 1.26/0.54 inference(evaluation,[],[f734])).
% 1.26/0.54 tff(f760,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x6,$sum($product(1000,$sum(x5,$sum(x4,x1))),X0)) = X0) )),
% 1.26/0.54 inference(backward_demodulation,[],[f625,f747])).
% 1.26/0.54 tff(f772,plain,(
% 1.26/0.54 0 = $sum(x4,x4)),
% 1.26/0.54 inference(backward_demodulation,[],[f620,f748])).
% 1.26/0.54 tff(f773,plain,(
% 1.26/0.54 0 = $sum(x5,x4)),
% 1.26/0.54 inference(backward_demodulation,[],[f632,f748])).
% 1.26/0.54 tff(f775,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x5,$sum(x4,X0)) = X0) )),
% 1.26/0.54 inference(backward_demodulation,[],[f653,f748])).
% 1.26/0.54 tff(f795,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(x6,$sum($product(1000,x1),X0)) = X0) )),
% 1.26/0.54 inference(backward_demodulation,[],[f760,f775])).
% 1.26/0.54 tff(f839,plain,(
% 1.26/0.54 x4 = $sum(x5,0)),
% 1.26/0.54 inference(superposition,[],[f775,f772])).
% 1.26/0.54 tff(f848,plain,(
% 1.26/0.54 x5 = x4),
% 1.26/0.54 inference(evaluation,[],[f839])).
% 1.26/0.54 tff(f859,plain,(
% 1.26/0.54 x5 = $sum(x1,x1)),
% 1.26/0.54 inference(backward_demodulation,[],[f746,f848])).
% 1.26/0.54 tff(f860,plain,(
% 1.26/0.54 x5 = x2),
% 1.26/0.54 inference(backward_demodulation,[],[f747,f848])).
% 1.26/0.54 tff(f861,plain,(
% 1.26/0.54 x5 = x3),
% 1.26/0.54 inference(backward_demodulation,[],[f748,f848])).
% 1.26/0.54 tff(f862,plain,(
% 1.26/0.54 0 = $sum(x5,x5)),
% 1.26/0.54 inference(backward_demodulation,[],[f773,f848])).
% 1.26/0.54 tff(f888,plain,(
% 1.26/0.54 $uminus($product(1000,x1)) = $sum(x6,0)),
% 1.26/0.54 inference(superposition,[],[f795,f25])).
% 1.26/0.54 tff(f890,plain,(
% 1.26/0.54 x6 = $uminus($product(1000,x1))),
% 1.26/0.54 inference(evaluation,[],[f888])).
% 1.26/0.54 tff(f925,plain,(
% 1.26/0.54 $product(1000,x1) = $uminus(x6)),
% 1.26/0.54 inference(superposition,[],[f31,f890])).
% 1.26/0.54 tff(f1477,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($product(X0,$sum(1,1)) = $sum(X0,X0)) )),
% 1.26/0.54 inference(superposition,[],[f385,f34])).
% 1.26/0.54 tff(f1504,plain,(
% 1.26/0.54 ( ! [X0 : $int] : ($sum(X0,X0) = $product(X0,2)) )),
% 1.26/0.54 inference(evaluation,[],[f1477])).
% 1.26/0.54 tff(f1511,plain,(
% 1.26/0.54 0 = $product(x5,2)),
% 1.26/0.54 inference(backward_demodulation,[],[f862,f1504])).
% 1.26/0.54 tff(f1512,plain,(
% 1.26/0.54 x5 = $product(x1,2)),
% 1.26/0.54 inference(backward_demodulation,[],[f859,f1504])).
% 1.26/0.54 tff(f1515,plain,(
% 1.26/0.54 x5 = $product(2,x1)),
% 1.26/0.54 inference(forward_demodulation,[],[f1512,f32])).
% 1.26/0.54 tff(f1516,plain,(
% 1.26/0.54 0 = $product(2,x5)),
% 1.26/0.54 inference(forward_demodulation,[],[f1511,f32])).
% 1.26/0.54 tff(f1521,plain,(
% 1.26/0.54 ( ! [X0 : $int] : (0 != $product(2,X0) | 0 = 2 | x5 = X0) )),
% 1.26/0.54 inference(superposition,[],[f62,f1516])).
% 1.26/0.54 tff(f1530,plain,(
% 1.26/0.54 ( ! [X0 : $int] : (0 != $product(2,X0) | x5 = X0) )),
% 1.26/0.54 inference(evaluation,[],[f1521])).
% 1.26/0.54 tff(f1543,plain,(
% 1.26/0.54 0 != 0 | x5 = 0),
% 1.26/0.54 inference(superposition,[],[f1530,f35])).
% 1.26/0.54 tff(f1544,plain,(
% 1.26/0.54 x5 = 0),
% 1.26/0.54 inference(trivial_inequality_removal,[],[f1543])).
% 1.26/0.54 tff(f1545,plain,(
% 1.26/0.54 spl0_5),
% 1.26/0.54 inference(avatar_split_clause,[],[f1544,f89])).
% 1.26/0.54 tff(f1546,plain,(
% 1.26/0.54 x4 = 0 | ~spl0_5),
% 1.26/0.54 inference(backward_demodulation,[],[f848,f90])).
% 1.26/0.54 tff(f1549,plain,(
% 1.26/0.54 x2 = 0 | ~spl0_5),
% 1.26/0.54 inference(backward_demodulation,[],[f860,f90])).
% 1.26/0.54 tff(f1550,plain,(
% 1.26/0.54 x3 = 0 | ~spl0_5),
% 1.26/0.54 inference(backward_demodulation,[],[f861,f90])).
% 1.26/0.54 tff(f1571,plain,(
% 1.26/0.54 0 = $product(2,x1) | ~spl0_5),
% 1.26/0.54 inference(backward_demodulation,[],[f1515,f90])).
% 1.26/0.54 tff(f1574,plain,(
% 1.26/0.54 ( ! [X0 : $int] : (0 != $product(2,X0) | 0 = X0) ) | ~spl0_5),
% 1.26/0.54 inference(backward_demodulation,[],[f1530,f90])).
% 1.26/0.54 tff(f1598,plain,(
% 1.26/0.54 spl0_3 | ~spl0_5),
% 1.26/0.54 inference(avatar_split_clause,[],[f1550,f89,f81])).
% 1.26/0.54 tff(f1599,plain,(
% 1.26/0.54 spl0_2 | ~spl0_5),
% 1.26/0.54 inference(avatar_split_clause,[],[f1549,f89,f77])).
% 1.26/0.54 tff(f1600,plain,(
% 1.26/0.54 spl0_4 | ~spl0_5),
% 1.26/0.54 inference(avatar_split_clause,[],[f1546,f89,f85])).
% 1.26/0.54 tff(f1625,plain,(
% 1.26/0.54 0 != 0 | x1 = 0 | ~spl0_5),
% 1.26/0.54 inference(superposition,[],[f1574,f1571])).
% 1.26/0.54 tff(f1644,plain,(
% 1.26/0.54 x1 = 0 | ~spl0_5),
% 1.26/0.54 inference(trivial_inequality_removal,[],[f1625])).
% 1.26/0.54 tff(f1648,plain,(
% 1.26/0.54 $false | (spl0_1 | ~spl0_5)),
% 1.26/0.54 inference(forward_subsumption_resolution,[],[f1644,f75])).
% 1.26/0.54 tff(f1649,plain,(
% 1.26/0.54 spl0_1 | ~spl0_5),
% 1.26/0.54 inference(avatar_contradiction_clause,[],[f1648])).
% 1.26/0.54 tff(f1656,plain,(
% 1.26/0.54 $uminus(x6) = $product(1000,0) | ~spl0_1),
% 1.26/0.54 inference(backward_demodulation,[],[f925,f74])).
% 1.26/0.54 tff(f1687,plain,(
% 1.26/0.54 0 = $uminus(x6) | ~spl0_1),
% 1.26/0.54 inference(evaluation,[],[f1656])).
% 1.26/0.54 tff(f1740,plain,(
% 1.26/0.54 0 = $sum(x6,0) | ~spl0_1),
% 1.26/0.54 inference(superposition,[],[f25,f1687])).
% 1.26/0.54 tff(f1753,plain,(
% 1.26/0.54 x6 = 0 | ~spl0_1),
% 1.26/0.54 inference(evaluation,[],[f1740])).
% 1.26/0.54 tff(f1759,plain,(
% 1.26/0.54 $false | (~spl0_1 | spl0_6)),
% 1.26/0.54 inference(forward_subsumption_resolution,[],[f1753,f95])).
% 1.26/0.54 tff(f1760,plain,(
% 1.26/0.54 ~spl0_1 | spl0_6),
% 1.26/0.54 inference(avatar_contradiction_clause,[],[f1759])).
% 1.26/0.54 cnf(s1, plain, ~spl0_1 | ~spl0_2 | ~spl0_3 | ~spl0_4 | ~spl0_5 | ~spl0_6, inference(sat_conversion,[],[f96])).
% 1.26/0.54 cnf(s2, plain, spl0_5, inference(sat_conversion,[],[f1545])).
% 1.26/0.54 cnf(s3, plain, spl0_3 | ~spl0_5, inference(sat_conversion,[],[f1598])).
% 1.26/0.54 cnf(s4, plain, spl0_2 | ~spl0_5, inference(sat_conversion,[],[f1599])).
% 1.26/0.54 cnf(s5, plain, spl0_4 | ~spl0_5, inference(sat_conversion,[],[f1600])).
% 1.26/0.54 cnf(s6, plain, spl0_1 | ~spl0_5, inference(sat_conversion,[],[f1649])).
% 1.26/0.54 cnf(s8, plain, ~spl0_1 | spl0_6, inference(sat_conversion,[],[f1760])).
% 1.26/0.54 cnf(s9, plain, spl0_1, inference(rat,[],[s6,s2])).
% 1.26/0.54 cnf(s10, plain, spl0_4, inference(rat,[],[s5,s2])).
% 1.26/0.54 cnf(s11, plain, spl0_2, inference(rat,[],[s4,s2])).
% 1.26/0.54 cnf(s12, plain, spl0_3, inference(rat,[],[s3,s2])).
% 1.26/0.54 cnf(s13, plain, spl0_6, inference(rat,[],[s8,s9])).
% 1.26/0.54 cnf(s14, plain, $false, inference(rat,[],[s1,s13,s2,s10,s12,s11,s9])).
% 1.26/0.54 tff(f1761,plain,(
% 1.26/0.54 $false),
% 1.26/0.54 inference(avatar_sat_refutation,[],[s14])).
% 1.26/0.54 % SZS output end Proof for theBenchmark
% 1.26/0.54 % (742933)------------------------------
% 1.26/0.54 % (742933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.26/0.54 % (742933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.26/0.54 % (742933)CaDiCaL version: 2.1.3
% 1.26/0.54 % (742933)Termination reason: Refutation
% 1.26/0.54 % (742933)Time elapsed: 0.103 s
% 1.26/0.54 % (742933)Peak memory usage: 13 MB
% 1.26/0.54 % (742933)Instructions burned: 103 (million)
% 1.26/0.54 % (742912)Success in time 0.209 s
% 1.26/0.54 % Vampire exiting
%------------------------------------------------------------------------------