%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW653_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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 01:40:35 PM UTC 2026
% Result : Theorem 0.20s 0.32s
% Output : Refutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW653_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n010.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 14:24:17 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.32 % (1955641)Will run a generic schedule for satisfiability detection.
% 0.20/0.32 % (1955660)dis+10_1_sil=32000:sp=arity:random_seed=2235025415:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.32 % (1955658)% WARNING: option uhcvi not known.
% 0.20/0.32 % (1955662)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3293072663:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.32 % (1955661)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=996166054:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.32 % (1955657)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2657734149_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.32 % (1955659)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2062749043:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.32 % (1955658)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2993904433:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.32 % (1955663)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4011065490:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.32 % (1955657)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.20/0.32 % (1955657)Terminated due to inappropriate strategy.
% 0.20/0.32 % (1955657)------------------------------
% 0.20/0.32 % (1955657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.32 % (1955657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.32 % (1955657)CaDiCaL version: 2.1.3
% 0.20/0.32 % (1955657)Termination reason: Inappropriate
% 0.20/0.32 % (1955657)Time elapsed: 0.002 s
% 0.20/0.32 % (1955657)Peak memory usage: 11 MB
% 0.20/0.32 % (1955657)Instructions burned: 4 (million)
% 0.20/0.32 % (1955657)------------------------------
% 0.20/0.32 % (1955657)------------------------------
% 0.20/0.32 % (1955681)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1516257736:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.20/0.32 % (1955681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.20/0.32 % (1955681)Terminated due to inappropriate strategy.
% 0.20/0.32 % (1955681)------------------------------
% 0.20/0.32 % (1955681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.32 % (1955681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.32 % (1955681)CaDiCaL version: 2.1.3
% 0.20/0.32 % (1955681)Termination reason: Inappropriate
% 0.20/0.32 % (1955681)Time elapsed: 0.002 s
% 0.20/0.32 % (1955681)Peak memory usage: 11 MB
% 0.20/0.32 % (1955681)Instructions burned: 3 (million)
% 0.20/0.32 % (1955681)------------------------------
% 0.20/0.32 % (1955681)------------------------------
% 0.20/0.32 % (1955660) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1955641-1955660"...
% 0.20/0.32 % (1955660)...printing done.
% 0.20/0.32 % (1955660)Refutation found. Thanks to Tanya!
% 0.20/0.32 % SZS status Theorem for theBenchmark
% 0.20/0.32 % SZS output start Proof for theBenchmark
% 0.20/0.32 tff(type_def_5, type, uni: $tType).
% 0.20/0.32 tff(type_def_6, type, ty: $tType).
% 0.20/0.32 tff(type_def_7, type, bool1: $tType).
% 0.20/0.32 tff(type_def_8, type, tuple02: $tType).
% 0.20/0.32 tff(type_def_9, type, uf_pure1: $tType).
% 0.20/0.32 tff(type_def_10, type, uf1: $tType).
% 0.20/0.32 tff(type_def_11, type, graph1: $tType).
% 0.20/0.32 tff(func_def_0, type, witness1: ty > uni).
% 0.20/0.32 tff(func_def_1, type, int: ty).
% 0.20/0.32 tff(func_def_2, type, real: ty).
% 0.20/0.32 tff(func_def_3, type, bool: ty).
% 0.20/0.32 tff(func_def_4, type, true1: bool1).
% 0.20/0.32 tff(func_def_5, type, false1: bool1).
% 0.20/0.32 tff(func_def_6, type, match_bool1: (ty * bool1 * uni * uni) > uni).
% 0.20/0.32 tff(func_def_7, type, tuple0: ty).
% 0.20/0.32 tff(func_def_8, type, tuple03: tuple02).
% 0.20/0.32 tff(func_def_9, type, qtmark: ty).
% 0.20/0.32 tff(func_def_12, type, ref: ty > ty).
% 0.20/0.32 tff(func_def_13, type, mk_ref: (ty * uni) > uni).
% 0.20/0.32 tff(func_def_14, type, contents: (ty * uni) > uni).
% 0.20/0.32 tff(func_def_15, type, uf_pure: ty).
% 0.20/0.32 tff(func_def_16, type, size1: uf_pure1 > $int).
% 0.20/0.32 tff(func_def_17, type, num1: uf_pure1 > $int).
% 0.20/0.32 tff(func_def_19, type, uf: ty).
% 0.20/0.32 tff(func_def_20, type, mk_uf1: uf_pure1 > uf1).
% 0.20/0.32 tff(func_def_21, type, state1: uf1 > uf_pure1).
% 0.20/0.32 tff(func_def_22, type, graph: ty).
% 0.20/0.32 tff(func_def_25, type, sK2: (uf_pure1 * $int) > $int).
% 0.20/0.32 tff(func_def_26, type, sK3: (uf_pure1 * $int * $int) > $int).
% 0.20/0.32 tff(func_def_27, type, sK4: (graph1 * $int * $int) > graph1).
% 0.20/0.32 tff(func_def_28, type, sK5: (graph1 * $int * $int) > $int).
% 0.20/0.32 tff(func_def_29, type, sK6: (graph1 * $int * $int) > $int).
% 0.20/0.32 tff(func_def_30, type, sK7: (graph1 * $int * $int) > graph1).
% 0.20/0.32 tff(func_def_31, type, sK8: (graph1 * $int * $int) > $int).
% 0.20/0.32 tff(func_def_32, type, sK9: (graph1 * $int * $int) > $int).
% 0.20/0.32 tff(func_def_33, type, sK10: (graph1 * $int * $int) > $int).
% 0.20/0.32 tff(func_def_34, type, sK11: (graph1 * $int * $int) > graph1).
% 0.20/0.32 tff(func_def_35, type, sK12: (graph1 * $int * $int) > $int).
% 0.20/0.32 tff(func_def_36, type, sK13: $int).
% 0.20/0.32 tff(func_def_37, type, sK14: $int).
% 0.20/0.32 tff(func_def_38, type, sK15: graph1).
% 0.20/0.32 tff(func_def_39, type, sK16: uf_pure1).
% 0.20/0.32 tff(func_def_40, type, sK17: $int).
% 0.20/0.32 tff(func_def_41, type, sK18: $int).
% 0.20/0.32 tff(pred_def_1, type, sort1: (ty * uni) > $o).
% 0.20/0.32 tff(pred_def_3, type, repr1: (uf_pure1 * $int * $int) > $o).
% 0.20/0.32 tff(pred_def_5, type, same1: (uf_pure1 * $int * $int) > $o).
% 0.20/0.32 tff(pred_def_6, type, same_reprs1: (uf_pure1 * uf_pure1) > $o).
% 0.20/0.32 tff(pred_def_7, type, path1: (graph1 * $int * $int) > $o).
% 0.20/0.32 tff(pred_def_8, type, sP0: (graph1 * $int * $int) > $o).
% 0.20/0.32 tff(pred_def_9, type, sP1: (graph1 * $int * $int) > $o).
% 0.20/0.32 tff(f8,axiom,(
% 0.20/0.32 ! [X0 : $int,X1 : $int,X2 : $int] : ($lesseq(X0,X1) => ($lesseq(0,X2) => $lesseq($product(X0,X2),$product(X1,X2))))),
% 0.20/0.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p',compatOrderMult)).
% 0.20/0.32 tff(f14,axiom,(
% 0.20/0.32 ! [X0 : uf_pure1,X1 : $int,X2 : $int,X3 : $int] : (($lesseq(0,X1) & $less(X1,size1(X0))) => (repr1(X0,X1,X2) => (repr1(X0,X1,X3) => X2 = X3)))),
% 0.20/0.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p',repr_function_2)).
% 0.20/0.32 tff(f15,axiom,(
% 0.20/0.32 ! [X0 : uf_pure1,X1 : $int,X2 : $int] : (same1(X0,X1,X2) <=> ! [X3 : $int] : (repr1(X0,X1,X3) <=> repr1(X0,X2,X3)))),
% 0.20/0.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p',same_def)).
% 0.20/0.32 tff(f25,conjecture,(
% 0.20/0.32 ! [X0 : $int,X1 : $int,X2 : graph1] : (($lesseq(1,X0) & X1 = 0 & ! [X3 : $int,X4 : $int] : (X3 = X4 <=> path1(X2,X3,X4))) => ($lesseq(0,$product(X0,X0)) => ! [X5 : uf_pure1] : ((num1(X5) = $product(X0,X0) & size1(X5) = $product(X0,X0) & ! [X3 : $int] : (($lesseq(0,X3) & $less(X3,$product(X0,X0))) => repr1(X5,X3,X3))) => (! [X3 : $int,X4 : $int] : (($lesseq(0,X3) & $less(X3,$product(X0,X0))) => (($lesseq(0,X4) & $less(X4,$product(X0,X0))) => (same1(X5,X3,X4) => (repr1(X5,X3,X4) & repr1(X5,X3,X3) & X3 = X4)))) => ($lesseq(1,num1(X5)) & $sum(num1(X5),X1) = size1(X5) & size1(X5) = $product(X0,X0) & ! [X3 : $int,X4 : $int] : (($lesseq(0,X3) & $less(X3,$product(X0,X0))) => (($lesseq(0,X4) & $less(X4,$product(X0,X0))) => (same1(X5,X3,X4) <=> path1(X2,X3,X4)))))))))),
% 0.20/0.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_build_maze)).
% 0.20/0.32 tff(f26,negated_conjecture,(
% 0.20/0.32 ~ ! [X0 : $int,X1 : $int,X2 : graph1] : (($lesseq(1,X0) & X1 = 0 & ! [X3 : $int,X4 : $int] : (X3 = X4 <=> path1(X2,X3,X4))) => ($lesseq(0,$product(X0,X0)) => ! [X5 : uf_pure1] : ((num1(X5) = $product(X0,X0) & size1(X5) = $product(X0,X0) & ! [X3 : $int] : (($lesseq(0,X3) & $less(X3,$product(X0,X0))) => repr1(X5,X3,X3))) => (! [X3 : $int,X4 : $int] : (($lesseq(0,X3) & $less(X3,$product(X0,X0))) => (($lesseq(0,X4) & $less(X4,$product(X0,X0))) => (same1(X5,X3,X4) => (repr1(X5,X3,X4) & repr1(X5,X3,X3) & X3 = X4)))) => ($lesseq(1,num1(X5)) & $sum(num1(X5),X1) = size1(X5) & size1(X5) = $product(X0,X0) & ! [X3 : $int,X4 : $int] : (($lesseq(0,X3) & $less(X3,$product(X0,X0))) => (($lesseq(0,X4) & $less(X4,$product(X0,X0))) => (same1(X5,X3,X4) <=> path1(X2,X3,X4)))))))))),
% 0.20/0.32 inference(negated_conjecture,[status(cth)],[f25])).
% 0.20/0.32 tff(f27,plain,(
% 0.20/0.32 ! [X0 : $int,X1 : $int,X2 : $int] : (~$less(X1,X0) => (~$less(X2,0) => ~$less($product(X1,X2),$product(X0,X2))))),
% 0.20/0.32 inference(theory_normalization,[],[f8])).
% 0.20/0.32 tff(f29,plain,(
% 0.20/0.32 ! [X0 : uf_pure1,X1 : $int,X2 : $int,X3 : $int] : ((~$less(X1,0) & $less(X1,size1(X0))) => (repr1(X0,X1,X2) => (repr1(X0,X1,X3) => X2 = X3)))),
% 0.20/0.32 inference(theory_normalization,[],[f14])).
% 0.20/0.32 tff(f32,plain,(
% 0.20/0.32 ~ ! [X0 : $int,X1 : $int,X2 : graph1] : ((~$less(X0,1) & X1 = 0 & ! [X3 : $int,X4 : $int] : (X3 = X4 <=> path1(X2,X3,X4))) => (~$less($product(X0,X0),0) => ! [X5 : uf_pure1] : ((num1(X5) = $product(X0,X0) & size1(X5) = $product(X0,X0) & ! [X3 : $int] : ((~$less(X3,0) & $less(X3,$product(X0,X0))) => repr1(X5,X3,X3))) => (! [X3 : $int,X4 : $int] : ((~$less(X3,0) & $less(X3,$product(X0,X0))) => ((~$less(X4,0) & $less(X4,$product(X0,X0))) => (same1(X5,X3,X4) => (repr1(X5,X3,X4) & repr1(X5,X3,X3) & X3 = X4)))) => (~$less(num1(X5),1) & $sum(num1(X5),X1) = size1(X5) & size1(X5) = $product(X0,X0) & ! [X3 : $int,X4 : $int] : ((~$less(X3,0) & $less(X3,$product(X0,X0))) => ((~$less(X4,0) & $less(X4,$product(X0,X0))) => (same1(X5,X3,X4) <=> path1(X2,X3,X4)))))))))),
% 0.20/0.32 inference(theory_normalization,[],[f26])).
% 0.20/0.32 tff(f39,definition,(
% 0.20/0.32 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 0.20/0.32 introduced(theory,[tha_transitivity])).
% 0.20/0.32 tff(f40,definition,(
% 0.20/0.32 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 0.20/0.32 introduced(theory,[tha_order_totality])).
% 0.20/0.32 tff(f44,definition,(
% 0.20/0.32 ( ! [X0 : $int,X1 : $int] : ($product(X1,X0) = $product(X0,X1)) )),
% 0.20/0.32 introduced(theory,[tha_commutativity])).
% 0.20/0.32 tff(f46,definition,(
% 0.20/0.32 ( ! [X0 : $int] : ($product(X0,1) = X0) )),
% 0.20/0.32 introduced(theory,[tha_right_identity])).
% 0.20/0.32 tff(f52,plain,(
% 0.20/0.32 ~ ! [X0 : $int,X1 : $int,X2 : graph1] : ((~$less(X0,1) & X1 = 0 & ! [X3 : $int,X4 : $int] : (X3 = X4 <=> path1(X2,X3,X4))) => (~$less($product(X0,X0),0) => ! [X5 : uf_pure1] : ((num1(X5) = $product(X0,X0) & size1(X5) = $product(X0,X0) & ! [X6 : $int] : ((~$less(X6,0) & $less(X6,$product(X0,X0))) => repr1(X5,X6,X6))) => (! [X7 : $int,X8 : $int] : ((~$less(X7,0) & $less(X7,$product(X0,X0))) => ((~$less(X8,0) & $less(X8,$product(X0,X0))) => (same1(X5,X7,X8) => (repr1(X5,X7,X8) & repr1(X5,X7,X7) & X7 = X8)))) => (~$less(num1(X5),1) & $sum(num1(X5),X1) = size1(X5) & size1(X5) = $product(X0,X0) & ! [X9 : $int,X10 : $int] : ((~$less(X9,0) & $less(X9,$product(X0,X0))) => ((~$less(X10,0) & $less(X10,$product(X0,X0))) => (same1(X5,X9,X10) <=> path1(X2,X9,X10)))))))))),
% 0.20/0.32 inference(rectify,[],[f32])).
% 0.20/0.32 tff(f55,plain,(
% 0.20/0.32 ! [X0 : $int,X1 : $int,X2 : $int] : ((~$less($product(X1,X2),$product(X0,X2)) | $less(X2,0)) | $less(X1,X0))),
% 0.20/0.32 inference(ennf_transformation,[],[f27])).
% 0.20/0.32 tff(f56,plain,(
% 0.20/0.32 ! [X0 : $int,X1 : $int,X2 : $int] : (~$less($product(X1,X2),$product(X0,X2)) | $less(X2,0) | $less(X1,X0))),
% 0.20/0.32 inference(flattening,[],[f55])).
% 0.20/0.32 tff(f61,plain,(
% 0.20/0.32 ! [X0 : uf_pure1,X1 : $int,X2 : $int,X3 : $int] : (((X2 = X3 | ~repr1(X0,X1,X3)) | ~repr1(X0,X1,X2)) | ($less(X1,0) | ~$less(X1,size1(X0))))),
% 0.20/0.32 inference(ennf_transformation,[],[f29])).
% 0.20/0.32 tff(f62,plain,(
% 0.20/0.32 ! [X0 : uf_pure1,X1 : $int,X2 : $int,X3 : $int] : (X2 = X3 | ~repr1(X0,X1,X3) | ~repr1(X0,X1,X2) | $less(X1,0) | ~$less(X1,size1(X0)))),
% 0.20/0.32 inference(flattening,[],[f61])).
% 0.20/0.32 tff(f72,plain,(
% 0.20/0.32 ? [X0 : $int,X1 : $int,X2 : graph1] : ((? [X5 : uf_pure1] : ((($less(num1(X5),1) | size1(X5) != $sum(num1(X5),X1) | $product(X0,X0) != size1(X5) | ? [X9 : $int,X10 : $int] : (((same1(X5,X9,X10) <~> path1(X2,X9,X10)) & (~$less(X10,0) & $less(X10,$product(X0,X0)))) & (~$less(X9,0) & $less(X9,$product(X0,X0))))) & ! [X7 : $int,X8 : $int] : ((((repr1(X5,X7,X8) & repr1(X5,X7,X7) & X7 = X8) | ~same1(X5,X7,X8)) | ($less(X8,0) | ~$less(X8,$product(X0,X0)))) | ($less(X7,0) | ~$less(X7,$product(X0,X0))))) & (num1(X5) = $product(X0,X0) & size1(X5) = $product(X0,X0) & ! [X6 : $int] : (repr1(X5,X6,X6) | ($less(X6,0) | ~$less(X6,$product(X0,X0)))))) & ~$less($product(X0,X0),0)) & (~$less(X0,1) & X1 = 0 & ! [X3 : $int,X4 : $int] : (X3 = X4 <=> path1(X2,X3,X4))))),
% 0.20/0.32 inference(ennf_transformation,[],[f52])).
% 0.20/0.32 tff(f73,plain,(
% 0.20/0.32 ? [X0 : $int,X1 : $int,X2 : graph1] : (? [X5 : uf_pure1] : (($less(num1(X5),1) | size1(X5) != $sum(num1(X5),X1) | $product(X0,X0) != size1(X5) | ? [X9 : $int,X10 : $int] : ((same1(X5,X9,X10) <~> path1(X2,X9,X10)) & ~$less(X10,0) & $less(X10,$product(X0,X0)) & ~$less(X9,0) & $less(X9,$product(X0,X0)))) & ! [X7 : $int,X8 : $int] : ((repr1(X5,X7,X8) & repr1(X5,X7,X7) & X7 = X8) | ~same1(X5,X7,X8) | $less(X8,0) | ~$less(X8,$product(X0,X0)) | $less(X7,0) | ~$less(X7,$product(X0,X0))) & num1(X5) = $product(X0,X0) & size1(X5) = $product(X0,X0) & ! [X6 : $int] : (repr1(X5,X6,X6) | $less(X6,0) | ~$less(X6,$product(X0,X0)))) & ~$less($product(X0,X0),0) & ~$less(X0,1) & X1 = 0 & ! [X3 : $int,X4 : $int] : (X3 = X4 <=> path1(X2,X3,X4)))),
% 0.20/0.32 inference(flattening,[],[f72])).
% 0.20/0.32 tff(f78,plain,(
% 0.20/0.32 ! [X0 : uf_pure1,X1 : $int,X2 : $int] : ((same1(X0,X1,X2) | ? [X3 : $int] : ((~repr1(X0,X2,X3) | ~repr1(X0,X1,X3)) & (repr1(X0,X2,X3) | repr1(X0,X1,X3)))) & (! [X3 : $int] : ((repr1(X0,X1,X3) | ~repr1(X0,X2,X3)) & (repr1(X0,X2,X3) | ~repr1(X0,X1,X3))) | ~same1(X0,X1,X2)))),
% 0.20/0.32 inference(nnf_transformation,[],[f15])).
% 0.20/0.32 tff(f79,plain,(
% 0.20/0.32 ! [X0 : uf_pure1,X1 : $int,X2 : $int] : ((same1(X0,X1,X2) | ? [X3 : $int] : ((~repr1(X0,X2,X3) | ~repr1(X0,X1,X3)) & (repr1(X0,X2,X3) | repr1(X0,X1,X3)))) & (! [X4 : $int] : ((repr1(X0,X1,X4) | ~repr1(X0,X2,X4)) & (repr1(X0,X2,X4) | ~repr1(X0,X1,X4))) | ~same1(X0,X1,X2)))),
% 0.20/0.32 inference(rectify,[],[f78])).
% 0.20/0.32 tff(f80,plain,(
% 0.20/0.32 ! [X0 : uf_pure1,X1 : $int,X2 : $int] : ((same1(X0,X1,X2) | ((~repr1(X0,X2,sK3(X0,X1,X2)) | ~repr1(X0,X1,sK3(X0,X1,X2))) & (repr1(X0,X2,sK3(X0,X1,X2)) | repr1(X0,X1,sK3(X0,X1,X2))))) & (! [X4 : $int] : ((repr1(X0,X1,X4) | ~repr1(X0,X2,X4)) & (repr1(X0,X2,X4) | ~repr1(X0,X1,X4))) | ~same1(X0,X1,X2)))),
% 0.20/0.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X3,sK3(X0,X1,X2))],[f79])).
% 0.20/0.32 tff(f88,plain,(
% 0.20/0.32 ? [X0 : $int,X1 : $int,X2 : graph1] : (? [X5 : uf_pure1] : (($less(num1(X5),1) | size1(X5) != $sum(num1(X5),X1) | $product(X0,X0) != size1(X5) | ? [X9 : $int,X10 : $int] : (((~path1(X2,X9,X10) | ~same1(X5,X9,X10)) & (path1(X2,X9,X10) | same1(X5,X9,X10))) & ~$less(X10,0) & $less(X10,$product(X0,X0)) & ~$less(X9,0) & $less(X9,$product(X0,X0)))) & ! [X7 : $int,X8 : $int] : ((repr1(X5,X7,X8) & repr1(X5,X7,X7) & X7 = X8) | ~same1(X5,X7,X8) | $less(X8,0) | ~$less(X8,$product(X0,X0)) | $less(X7,0) | ~$less(X7,$product(X0,X0))) & num1(X5) = $product(X0,X0) & size1(X5) = $product(X0,X0) & ! [X6 : $int] : (repr1(X5,X6,X6) | $less(X6,0) | ~$less(X6,$product(X0,X0)))) & ~$less($product(X0,X0),0) & ~$less(X0,1) & X1 = 0 & ! [X3 : $int,X4 : $int] : ((X3 = X4 | ~path1(X2,X3,X4)) & (path1(X2,X3,X4) | X3 != X4)))),
% 0.20/0.32 inference(nnf_transformation,[],[f73])).
% 0.20/0.32 tff(f89,plain,(
% 0.20/0.32 ? [X0 : $int,X1 : $int,X2 : graph1] : (? [X5 : uf_pure1] : (($less(num1(X5),1) | size1(X5) != $sum(num1(X5),X1) | $product(X0,X0) != size1(X5) | ? [X9 : $int,X10 : $int] : ((~path1(X2,X9,X10) | ~same1(X5,X9,X10)) & (path1(X2,X9,X10) | same1(X5,X9,X10)) & ~$less(X10,0) & $less(X10,$product(X0,X0)) & ~$less(X9,0) & $less(X9,$product(X0,X0)))) & ! [X7 : $int,X8 : $int] : ((repr1(X5,X7,X8) & repr1(X5,X7,X7) & X7 = X8) | ~same1(X5,X7,X8) | $less(X8,0) | ~$less(X8,$product(X0,X0)) | $less(X7,0) | ~$less(X7,$product(X0,X0))) & num1(X5) = $product(X0,X0) & size1(X5) = $product(X0,X0) & ! [X6 : $int] : (repr1(X5,X6,X6) | $less(X6,0) | ~$less(X6,$product(X0,X0)))) & ~$less($product(X0,X0),0) & ~$less(X0,1) & X1 = 0 & ! [X3 : $int,X4 : $int] : ((X3 = X4 | ~path1(X2,X3,X4)) & (path1(X2,X3,X4) | X3 != X4)))),
% 0.20/0.32 inference(flattening,[],[f88])).
% 0.20/0.32 tff(f90,plain,(
% 0.20/0.32 ? [X0 : $int,X1 : $int,X2 : graph1] : (? [X3 : uf_pure1] : (($less(num1(X3),1) | size1(X3) != $sum(num1(X3),X1) | $product(X0,X0) != size1(X3) | ? [X4 : $int,X5 : $int] : ((~path1(X2,X4,X5) | ~same1(X3,X4,X5)) & (path1(X2,X4,X5) | same1(X3,X4,X5)) & ~$less(X5,0) & $less(X5,$product(X0,X0)) & ~$less(X4,0) & $less(X4,$product(X0,X0)))) & ! [X6 : $int,X7 : $int] : ((repr1(X3,X6,X7) & repr1(X3,X6,X6) & X6 = X7) | ~same1(X3,X6,X7) | $less(X7,0) | ~$less(X7,$product(X0,X0)) | $less(X6,0) | ~$less(X6,$product(X0,X0))) & $product(X0,X0) = num1(X3) & $product(X0,X0) = size1(X3) & ! [X8 : $int] : (repr1(X3,X8,X8) | $less(X8,0) | ~$less(X8,$product(X0,X0)))) & ~$less($product(X0,X0),0) & ~$less(X0,1) & X1 = 0 & ! [X9 : $int,X10 : $int] : ((X9 = X10 | ~path1(X2,X9,X10)) & (path1(X2,X9,X10) | X9 != X10)))),
% 0.20/0.32 inference(rectify,[],[f89])).
% 0.20/0.32 tff(f91,plain,(
% 0.20/0.32 (($less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),sK14) | size1(sK16) != $product(sK13,sK13) | ((~path1(sK15,sK17,sK18) | ~same1(sK16,sK17,sK18)) & (path1(sK15,sK17,sK18) | same1(sK16,sK17,sK18)) & ~$less(sK18,0) & $less(sK18,$product(sK13,sK13)) & ~$less(sK17,0) & $less(sK17,$product(sK13,sK13)))) & ! [X6 : $int,X7 : $int] : ((repr1(sK16,X6,X7) & repr1(sK16,X6,X6) & X6 = X7) | ~same1(sK16,X6,X7) | $less(X7,0) | ~$less(X7,$product(sK13,sK13)) | $less(X6,0) | ~$less(X6,$product(sK13,sK13))) & num1(sK16) = $product(sK13,sK13) & size1(sK16) = $product(sK13,sK13) & ! [X8 : $int] : (repr1(sK16,X8,X8) | $less(X8,0) | ~$less(X8,$product(sK13,sK13)))) & ~$less($product(sK13,sK13),0) & ~$less(sK13,1) & 0 = sK14 & ! [X9 : $int,X10 : $int] : ((X9 = X10 | ~path1(sK15,X9,X10)) & (path1(sK15,X9,X10) | X9 != X10))),
% 0.20/0.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16,sK17,sK18]),skolemize(X0,sK13),skolemize(X1,sK14),skolemize(X2,sK15),skolemize(X3,sK16),skolemize(X4,sK17),skolemize(X5,sK18)],[f90])).
% 0.20/0.32 tff(f99,plain,(
% 0.20/0.32 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less($product(X1,X2),$product(X0,X2)) | $less(X2,0) | $less(X1,X0)) )),
% 0.20/0.32 inference(cnf_transformation,[],[f56])).
% 0.20/0.32 tff(f107,plain,(
% 0.20/0.32 ( ! [X2 : $int,X3 : $int,X0 : uf_pure1,X1 : $int] : (~$less(X1,size1(X0)) | ~repr1(X0,X1,X3) | ~repr1(X0,X1,X2) | $less(X1,0) | X2 = X3) )),
% 0.20/0.32 inference(cnf_transformation,[],[f62])).
% 0.20/0.32 tff(f110,plain,(
% 0.20/0.32 ( ! [X2 : $int,X0 : uf_pure1,X1 : $int] : (repr1(X0,X2,sK3(X0,X1,X2)) | repr1(X0,X1,sK3(X0,X1,X2)) | same1(X0,X1,X2)) )),
% 0.20/0.32 inference(cnf_transformation,[],[f80])).
% 0.20/0.32 tff(f111,plain,(
% 0.20/0.32 ( ! [X2 : $int,X0 : uf_pure1,X1 : $int] : (~repr1(X0,X2,sK3(X0,X1,X2)) | same1(X0,X1,X2) | ~repr1(X0,X1,sK3(X0,X1,X2))) )),
% 0.20/0.32 inference(cnf_transformation,[],[f80])).
% 0.20/0.32 tff(f132,plain,(
% 0.20/0.32 ( ! [X10 : $int,X9 : $int] : (path1(sK15,X9,X10) | X9 != X10) )),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f133,plain,(
% 0.20/0.32 ( ! [X10 : $int,X9 : $int] : (~path1(sK15,X9,X10) | X9 = X10) )),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f134,plain,(
% 0.20/0.32 0 = sK14),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f135,plain,(
% 0.20/0.32 ~$less(sK13,1)),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f137,plain,(
% 0.20/0.32 ( ! [X8 : $int] : (repr1(sK16,X8,X8) | $less(X8,0) | ~$less(X8,$product(sK13,sK13))) )),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f138,plain,(
% 0.20/0.32 size1(sK16) = $product(sK13,sK13)),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f139,plain,(
% 0.20/0.32 num1(sK16) = $product(sK13,sK13)),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f140,plain,(
% 0.20/0.32 ( ! [X6 : $int,X7 : $int] : (X6 = X7 | ~same1(sK16,X6,X7) | $less(X7,0) | ~$less(X7,$product(sK13,sK13)) | $less(X6,0) | ~$less(X6,$product(sK13,sK13))) )),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f143,plain,(
% 0.20/0.32 $less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),sK14) | size1(sK16) != $product(sK13,sK13) | $less(sK17,$product(sK13,sK13))),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f144,plain,(
% 0.20/0.32 $less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),sK14) | size1(sK16) != $product(sK13,sK13) | ~$less(sK17,0)),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f145,plain,(
% 0.20/0.32 $less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),sK14) | size1(sK16) != $product(sK13,sK13) | $less(sK18,$product(sK13,sK13))),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f146,plain,(
% 0.20/0.32 $less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),sK14) | size1(sK16) != $product(sK13,sK13) | ~$less(sK18,0)),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f147,plain,(
% 0.20/0.32 $less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),sK14) | size1(sK16) != $product(sK13,sK13) | path1(sK15,sK17,sK18) | same1(sK16,sK17,sK18)),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f148,plain,(
% 0.20/0.32 $less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),sK14) | size1(sK16) != $product(sK13,sK13) | ~path1(sK15,sK17,sK18) | ~same1(sK16,sK17,sK18)),
% 0.20/0.32 inference(cnf_transformation,[],[f91])).
% 0.20/0.32 tff(f149,plain,(
% 0.20/0.32 $less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),0) | size1(sK16) != $product(sK13,sK13) | ~path1(sK15,sK17,sK18) | ~same1(sK16,sK17,sK18)),
% 0.20/0.32 inference(definition_unfolding,[],[f148,f134])).
% 0.20/0.32 tff(f150,plain,(
% 0.20/0.32 $less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),0) | size1(sK16) != $product(sK13,sK13) | path1(sK15,sK17,sK18) | same1(sK16,sK17,sK18)),
% 0.20/0.32 inference(definition_unfolding,[],[f147,f134])).
% 0.20/0.32 tff(f151,plain,(
% 0.20/0.32 $less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),0) | size1(sK16) != $product(sK13,sK13) | ~$less(sK18,0)),
% 0.20/0.32 inference(definition_unfolding,[],[f146,f134])).
% 0.20/0.32 tff(f152,plain,(
% 0.20/0.32 $less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),0) | size1(sK16) != $product(sK13,sK13) | $less(sK18,$product(sK13,sK13))),
% 0.20/0.32 inference(definition_unfolding,[],[f145,f134])).
% 0.20/0.32 tff(f153,plain,(
% 0.20/0.32 $less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),0) | size1(sK16) != $product(sK13,sK13) | ~$less(sK17,0)),
% 0.20/0.32 inference(definition_unfolding,[],[f144,f134])).
% 0.20/0.32 tff(f154,plain,(
% 0.20/0.32 $less(num1(sK16),1) | size1(sK16) != $sum(num1(sK16),0) | size1(sK16) != $product(sK13,sK13) | $less(sK17,$product(sK13,sK13))),
% 0.20/0.32 inference(definition_unfolding,[],[f143,f134])).
% 0.20/0.32 tff(f156,plain,(
% 0.20/0.32 ( ! [X10 : $int] : (path1(sK15,X10,X10)) )),
% 0.20/0.32 inference(equality_resolution,[],[f132])).
% 0.20/0.32 tff(f157,plain,(
% 0.20/0.32 $less(num1(sK16),1) | num1(sK16) != size1(sK16) | size1(sK16) != $product(sK13,sK13) | $less(sK17,$product(sK13,sK13))),
% 0.20/0.32 inference(evaluation,[],[f154])).
% 0.20/0.32 tff(f158,plain,(
% 0.20/0.32 $less(num1(sK16),1) | num1(sK16) != size1(sK16) | size1(sK16) != $product(sK13,sK13) | ~$less(sK17,0)),
% 0.20/0.32 inference(evaluation,[],[f153])).
% 0.20/0.32 tff(f159,plain,(
% 0.20/0.32 $less(num1(sK16),1) | num1(sK16) != size1(sK16) | size1(sK16) != $product(sK13,sK13) | $less(sK18,$product(sK13,sK13))),
% 0.20/0.32 inference(evaluation,[],[f152])).
% 0.20/0.32 tff(f160,plain,(
% 0.20/0.32 $less(num1(sK16),1) | num1(sK16) != size1(sK16) | size1(sK16) != $product(sK13,sK13) | ~$less(sK18,0)),
% 0.20/0.32 inference(evaluation,[],[f151])).
% 0.20/0.32 tff(f161,plain,(
% 0.20/0.32 $less(num1(sK16),1) | num1(sK16) != size1(sK16) | size1(sK16) != $product(sK13,sK13) | path1(sK15,sK17,sK18) | same1(sK16,sK17,sK18)),
% 0.20/0.32 inference(evaluation,[],[f150])).
% 0.20/0.32 tff(f162,plain,(
% 0.20/0.32 $less(num1(sK16),1) | num1(sK16) != size1(sK16) | size1(sK16) != $product(sK13,sK13) | ~path1(sK15,sK17,sK18) | ~same1(sK16,sK17,sK18)),
% 0.20/0.32 inference(evaluation,[],[f149])).
% 0.20/0.32 tff(f164,definition,(
% 0.20/0.32 spl19_1 <=> $less(sK17,$product(sK13,sK13))),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_1])],[avatar_definition])).
% 0.20/0.32 tff(f166,plain,(
% 0.20/0.32 $less(sK17,$product(sK13,sK13)) | ~spl19_1),
% 0.20/0.32 inference(avatar_component_clause,[],[f164])).
% 0.20/0.32 tff(f168,definition,(
% 0.20/0.32 spl19_2 <=> size1(sK16) = $product(sK13,sK13)),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_2])],[avatar_definition])).
% 0.20/0.32 tff(f169,plain,(
% 0.20/0.32 size1(sK16) = $product(sK13,sK13) | ~spl19_2),
% 0.20/0.32 inference(avatar_component_clause,[],[f168])).
% 0.20/0.32 tff(f172,definition,(
% 0.20/0.32 spl19_3 <=> num1(sK16) = size1(sK16)),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_3])],[avatar_definition])).
% 0.20/0.32 tff(f173,plain,(
% 0.20/0.32 num1(sK16) = size1(sK16) | ~spl19_3),
% 0.20/0.32 inference(avatar_component_clause,[],[f172])).
% 0.20/0.32 tff(f176,definition,(
% 0.20/0.32 spl19_4 <=> $less(num1(sK16),1)),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_4])],[avatar_definition])).
% 0.20/0.32 tff(f178,plain,(
% 0.20/0.32 $less(num1(sK16),1) | ~spl19_4),
% 0.20/0.32 inference(avatar_component_clause,[],[f176])).
% 0.20/0.32 tff(f179,plain,(
% 0.20/0.32 spl19_1 | ~spl19_2 | ~spl19_3 | spl19_4),
% 0.20/0.32 inference(avatar_split_clause,[],[f157,f176,f172,f168,f164])).
% 0.20/0.32 tff(f181,definition,(
% 0.20/0.32 spl19_5 <=> $less(sK17,0)),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_5])],[avatar_definition])).
% 0.20/0.32 tff(f183,plain,(
% 0.20/0.32 ~$less(sK17,0) | spl19_5),
% 0.20/0.32 inference(avatar_component_clause,[],[f181])).
% 0.20/0.32 tff(f184,plain,(
% 0.20/0.32 ~spl19_5 | ~spl19_2 | ~spl19_3 | spl19_4),
% 0.20/0.32 inference(avatar_split_clause,[],[f158,f176,f172,f168,f181])).
% 0.20/0.32 tff(f186,definition,(
% 0.20/0.32 spl19_6 <=> $less(sK18,$product(sK13,sK13))),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_6])],[avatar_definition])).
% 0.20/0.32 tff(f188,plain,(
% 0.20/0.32 $less(sK18,$product(sK13,sK13)) | ~spl19_6),
% 0.20/0.32 inference(avatar_component_clause,[],[f186])).
% 0.20/0.32 tff(f189,plain,(
% 0.20/0.32 spl19_6 | ~spl19_2 | ~spl19_3 | spl19_4),
% 0.20/0.32 inference(avatar_split_clause,[],[f159,f176,f172,f168,f186])).
% 0.20/0.32 tff(f191,definition,(
% 0.20/0.32 spl19_7 <=> $less(sK18,0)),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_7])],[avatar_definition])).
% 0.20/0.32 tff(f193,plain,(
% 0.20/0.32 ~$less(sK18,0) | spl19_7),
% 0.20/0.32 inference(avatar_component_clause,[],[f191])).
% 0.20/0.32 tff(f194,plain,(
% 0.20/0.32 ~spl19_7 | ~spl19_2 | ~spl19_3 | spl19_4),
% 0.20/0.32 inference(avatar_split_clause,[],[f160,f176,f172,f168,f191])).
% 0.20/0.32 tff(f196,definition,(
% 0.20/0.32 spl19_8 <=> same1(sK16,sK17,sK18)),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_8])],[avatar_definition])).
% 0.20/0.32 tff(f197,plain,(
% 0.20/0.32 ~same1(sK16,sK17,sK18) | spl19_8),
% 0.20/0.32 inference(avatar_component_clause,[],[f196])).
% 0.20/0.32 tff(f198,plain,(
% 0.20/0.32 same1(sK16,sK17,sK18) | ~spl19_8),
% 0.20/0.32 inference(avatar_component_clause,[],[f196])).
% 0.20/0.32 tff(f200,definition,(
% 0.20/0.32 spl19_9 <=> path1(sK15,sK17,sK18)),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_9])],[avatar_definition])).
% 0.20/0.32 tff(f201,plain,(
% 0.20/0.32 ~path1(sK15,sK17,sK18) | spl19_9),
% 0.20/0.32 inference(avatar_component_clause,[],[f200])).
% 0.20/0.32 tff(f202,plain,(
% 0.20/0.32 path1(sK15,sK17,sK18) | ~spl19_9),
% 0.20/0.32 inference(avatar_component_clause,[],[f200])).
% 0.20/0.32 tff(f203,plain,(
% 0.20/0.32 spl19_8 | spl19_9 | ~spl19_2 | ~spl19_3 | spl19_4),
% 0.20/0.32 inference(avatar_split_clause,[],[f161,f176,f172,f168,f200,f196])).
% 0.20/0.32 tff(f204,plain,(
% 0.20/0.32 ~spl19_8 | ~spl19_9 | ~spl19_2 | ~spl19_3 | spl19_4),
% 0.20/0.32 inference(avatar_split_clause,[],[f162,f176,f172,f168,f200,f196])).
% 0.20/0.32 tff(f205,plain,(
% 0.20/0.32 spl19_2),
% 0.20/0.32 inference(avatar_split_clause,[],[f138,f168])).
% 0.20/0.32 tff(f208,plain,(
% 0.20/0.32 num1(sK16) = size1(sK16) | ~spl19_2),
% 0.20/0.32 inference(superposition,[],[f139,f169])).
% 0.20/0.32 tff(f214,plain,(
% 0.20/0.32 spl19_3 | ~spl19_2),
% 0.20/0.32 inference(avatar_split_clause,[],[f208,f168,f172])).
% 0.20/0.32 tff(f215,plain,(
% 0.20/0.32 $less(size1(sK16),1) | (~spl19_3 | ~spl19_4)),
% 0.20/0.32 inference(superposition,[],[f178,f173])).
% 0.20/0.32 tff(f218,plain,(
% 0.20/0.32 ( ! [X8 : $int] : (~$less(X8,num1(sK16)) | repr1(sK16,X8,X8) | $less(X8,0)) )),
% 0.20/0.32 inference(forward_demodulation,[],[f137,f139])).
% 0.20/0.32 tff(f219,plain,(
% 0.20/0.32 ( ! [X8 : $int] : (~$less(X8,size1(sK16)) | repr1(sK16,X8,X8) | $less(X8,0)) ) | ~spl19_3),
% 0.20/0.32 inference(forward_demodulation,[],[f218,f173])).
% 0.20/0.32 tff(f220,plain,(
% 0.20/0.32 ( ! [X6 : $int,X7 : $int] : (~$less(X7,num1(sK16)) | X6 = X7 | ~same1(sK16,X6,X7) | $less(X7,0) | $less(X6,0) | ~$less(X6,$product(sK13,sK13))) )),
% 0.20/0.32 inference(forward_demodulation,[],[f140,f139])).
% 0.20/0.32 tff(f221,plain,(
% 0.20/0.32 ( ! [X6 : $int,X7 : $int] : (~$less(X7,size1(sK16)) | X6 = X7 | ~same1(sK16,X6,X7) | $less(X7,0) | $less(X6,0) | ~$less(X6,$product(sK13,sK13))) ) | ~spl19_3),
% 0.20/0.32 inference(forward_demodulation,[],[f220,f173])).
% 0.20/0.32 tff(f222,plain,(
% 0.20/0.32 ( ! [X6 : $int,X7 : $int] : (~$less(X6,num1(sK16)) | ~$less(X7,size1(sK16)) | X6 = X7 | ~same1(sK16,X6,X7) | $less(X7,0) | $less(X6,0)) ) | ~spl19_3),
% 0.20/0.32 inference(forward_demodulation,[],[f221,f139])).
% 0.20/0.32 tff(f223,plain,(
% 0.20/0.32 ( ! [X6 : $int,X7 : $int] : (~same1(sK16,X6,X7) | ~$less(X7,size1(sK16)) | X6 = X7 | ~$less(X6,size1(sK16)) | $less(X7,0) | $less(X6,0)) ) | ~spl19_3),
% 0.20/0.32 inference(forward_demodulation,[],[f222,f173])).
% 0.20/0.32 tff(f282,plain,(
% 0.20/0.32 $less(1,sK13) | 1 = sK13),
% 0.20/0.32 inference(resolution,[],[f40,f135])).
% 0.20/0.32 tff(f293,definition,(
% 0.20/0.32 spl19_10 <=> 1 = sK13),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_10])],[avatar_definition])).
% 0.20/0.32 tff(f295,plain,(
% 0.20/0.32 1 = sK13 | ~spl19_10),
% 0.20/0.32 inference(avatar_component_clause,[],[f293])).
% 0.20/0.32 tff(f297,definition,(
% 0.20/0.32 spl19_11 <=> $less(1,sK13)),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_11])],[avatar_definition])).
% 0.20/0.32 tff(f299,plain,(
% 0.20/0.32 $less(1,sK13) | ~spl19_11),
% 0.20/0.32 inference(avatar_component_clause,[],[f297])).
% 0.20/0.32 tff(f312,plain,(
% 0.20/0.32 spl19_10 | spl19_11),
% 0.20/0.32 inference(avatar_split_clause,[],[f282,f297,f293])).
% 0.20/0.32 tff(f329,plain,(
% 0.20/0.32 num1(sK16) = $product(1,1) | ~spl19_10),
% 0.20/0.32 inference(superposition,[],[f139,f295])).
% 0.20/0.32 tff(f332,plain,(
% 0.20/0.32 1 = num1(sK16) | ~spl19_10),
% 0.20/0.32 inference(evaluation,[],[f329])).
% 0.20/0.32 tff(f367,plain,(
% 0.20/0.32 $less(1,1) | (~spl19_4 | ~spl19_10)),
% 0.20/0.32 inference(superposition,[],[f178,f332])).
% 0.20/0.32 tff(f369,plain,(
% 0.20/0.32 $false | (~spl19_4 | ~spl19_10)),
% 0.20/0.32 inference(evaluation,[],[f367])).
% 0.20/0.32 tff(f370,plain,(
% 0.20/0.32 ~spl19_4 | ~spl19_10),
% 0.20/0.32 inference(avatar_contradiction_clause,[],[f369])).
% 0.20/0.32 tff(f385,plain,(
% 0.20/0.32 ( ! [X0 : $int] : (~$less(X0,1) | $less(X0,sK13)) ) | ~spl19_11),
% 0.20/0.32 inference(resolution,[],[f299,f39])).
% 0.20/0.32 tff(f391,plain,(
% 0.20/0.32 $less(size1(sK16),sK13) | (~spl19_3 | ~spl19_4 | ~spl19_11)),
% 0.20/0.32 inference(resolution,[],[f385,f215])).
% 0.20/0.32 tff(f575,plain,(
% 0.20/0.32 ( ! [X0 : $int] : (~$less(num1(sK16),$product(X0,sK13)) | $less(sK13,0) | $less(sK13,X0)) )),
% 0.20/0.32 inference(superposition,[],[f99,f139])).
% 0.20/0.32 tff(f600,plain,(
% 0.20/0.32 ( ! [X0 : $int] : (~$less(size1(sK16),$product(X0,sK13)) | $less(sK13,0) | $less(sK13,X0)) ) | ~spl19_3),
% 0.20/0.32 inference(forward_demodulation,[],[f575,f173])).
% 0.20/0.32 tff(f604,definition,(
% 0.20/0.32 spl19_14 <=> $less(sK13,0)),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_14])],[avatar_definition])).
% 0.20/0.32 tff(f606,plain,(
% 0.20/0.32 $less(sK13,0) | ~spl19_14),
% 0.20/0.32 inference(avatar_component_clause,[],[f604])).
% 0.20/0.32 tff(f623,definition,(
% 0.20/0.32 spl19_18 <=> ! [X0 : $int] : (~$less(size1(sK16),$product(X0,sK13)) | $less(sK13,X0))),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_18])],[avatar_definition])).
% 0.20/0.32 tff(f624,plain,(
% 0.20/0.32 ( ! [X0 : $int] : (~$less(size1(sK16),$product(X0,sK13)) | $less(sK13,X0)) ) | ~spl19_18),
% 0.20/0.32 inference(avatar_component_clause,[],[f623])).
% 0.20/0.32 tff(f627,plain,(
% 0.20/0.32 spl19_14 | spl19_18 | ~spl19_3),
% 0.20/0.32 inference(avatar_split_clause,[],[f600,f172,f623,f604])).
% 0.20/0.32 tff(f628,plain,(
% 0.20/0.32 ( ! [X0 : $int] : (~$less(X0,sK13) | $less(X0,0)) ) | ~spl19_14),
% 0.20/0.32 inference(resolution,[],[f606,f39])).
% 0.20/0.32 tff(f698,plain,(
% 0.20/0.32 ( ! [X0 : uf_pure1,X1 : $int] : (repr1(X0,X1,sK3(X0,X1,X1)) | same1(X0,X1,X1)) )),
% 0.20/0.32 inference(factoring,[],[f110])).
% 0.20/0.32 tff(f699,plain,(
% 0.20/0.32 $less(1,0) | (~spl19_11 | ~spl19_14)),
% 0.20/0.32 inference(resolution,[],[f628,f299])).
% 0.20/0.32 tff(f704,plain,(
% 0.20/0.32 $false | (~spl19_11 | ~spl19_14)),
% 0.20/0.32 inference(evaluation,[],[f699])).
% 0.20/0.32 tff(f705,plain,(
% 0.20/0.32 ~spl19_11 | ~spl19_14),
% 0.20/0.32 inference(avatar_contradiction_clause,[],[f704])).
% 0.20/0.32 tff(f824,plain,(
% 0.20/0.32 ( ! [X0 : $int] : (~$less(size1(sK16),$product(sK13,X0)) | $less(sK13,X0)) ) | ~spl19_18),
% 0.20/0.32 inference(superposition,[],[f624,f44])).
% 0.20/0.32 tff(f890,plain,(
% 0.20/0.32 ~$less(size1(sK16),sK13) | $less(sK13,1) | ~spl19_18),
% 0.20/0.32 inference(superposition,[],[f824,f46])).
% 0.20/0.32 tff(f894,plain,(
% 0.20/0.32 $less(sK13,1) | (~spl19_3 | ~spl19_4 | ~spl19_11 | ~spl19_18)),
% 0.20/0.32 inference(forward_subsumption_resolution,[],[f890,f391])).
% 0.20/0.32 tff(f896,plain,(
% 0.20/0.32 $false | (~spl19_3 | ~spl19_4 | ~spl19_11 | ~spl19_18)),
% 0.20/0.32 inference(forward_subsumption_resolution,[],[f894,f135])).
% 0.20/0.32 tff(f897,plain,(
% 0.20/0.32 ~spl19_3 | ~spl19_4 | ~spl19_11 | ~spl19_18),
% 0.20/0.32 inference(avatar_contradiction_clause,[],[f896])).
% 0.20/0.32 tff(f899,plain,(
% 0.20/0.32 $less(sK17,num1(sK16)) | ~spl19_1),
% 0.20/0.32 inference(forward_demodulation,[],[f166,f139])).
% 0.20/0.32 tff(f901,plain,(
% 0.20/0.32 $less(sK18,num1(sK16)) | ~spl19_6),
% 0.20/0.32 inference(forward_demodulation,[],[f188,f139])).
% 0.20/0.32 tff(f903,plain,(
% 0.20/0.32 $less(sK17,size1(sK16)) | (~spl19_1 | ~spl19_3)),
% 0.20/0.32 inference(forward_demodulation,[],[f899,f173])).
% 0.20/0.32 tff(f904,plain,(
% 0.20/0.32 $less(sK18,size1(sK16)) | (~spl19_3 | ~spl19_6)),
% 0.20/0.32 inference(forward_demodulation,[],[f901,f173])).
% 0.20/0.32 tff(f930,plain,(
% 0.20/0.32 sK17 = sK18 | ~spl19_9),
% 0.20/0.32 inference(resolution,[],[f202,f133])).
% 0.20/0.32 tff(f966,plain,(
% 0.20/0.32 ~same1(sK16,sK17,sK17) | (spl19_8 | ~spl19_9)),
% 0.20/0.32 inference(superposition,[],[f197,f930])).
% 0.20/0.32 tff(f968,plain,(
% 0.20/0.32 repr1(sK16,sK17,sK17) | $less(sK17,0) | (~spl19_1 | ~spl19_3)),
% 0.20/0.32 inference(resolution,[],[f903,f219])).
% 0.20/0.32 tff(f969,plain,(
% 0.20/0.32 ( ! [X0 : $int,X1 : $int] : (~repr1(sK16,sK17,X0) | ~repr1(sK16,sK17,X1) | $less(sK17,0) | X0 = X1) ) | (~spl19_1 | ~spl19_3)),
% 0.20/0.32 inference(resolution,[],[f903,f107])).
% 0.20/0.32 tff(f971,plain,(
% 0.20/0.32 ( ! [X0 : $int,X1 : $int] : (~repr1(sK16,sK17,X1) | ~repr1(sK16,sK17,X0) | X0 = X1) ) | (~spl19_1 | ~spl19_3 | spl19_5)),
% 0.20/0.32 inference(forward_subsumption_resolution,[],[f969,f183])).
% 0.20/0.32 tff(f972,plain,(
% 0.20/0.32 repr1(sK16,sK17,sK17) | (~spl19_1 | ~spl19_3 | spl19_5)),
% 0.20/0.32 inference(forward_subsumption_resolution,[],[f968,f183])).
% 0.20/0.32 tff(f991,plain,(
% 0.20/0.32 ( ! [X0 : $int] : (~repr1(sK16,sK17,X0) | sK17 = X0) ) | (~spl19_1 | ~spl19_3 | spl19_5)),
% 0.20/0.32 inference(resolution,[],[f971,f972])).
% 0.20/0.32 tff(f1040,definition,(
% 0.20/0.32 spl19_32 <=> ! [X0 : $int] : (~repr1(sK16,sK17,X0) | sK17 = X0)),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_32])],[avatar_definition])).
% 0.20/0.32 tff(f1041,plain,(
% 0.20/0.32 ( ! [X0 : $int] : (~repr1(sK16,sK17,X0) | sK17 = X0) ) | ~spl19_32),
% 0.20/0.32 inference(avatar_component_clause,[],[f1040])).
% 0.20/0.32 tff(f1078,plain,(
% 0.20/0.32 spl19_32 | ~spl19_1 | ~spl19_3 | spl19_5),
% 0.20/0.32 inference(avatar_split_clause,[],[f991,f181,f172,f164,f1040])).
% 0.20/0.32 tff(f2258,plain,(
% 0.20/0.32 same1(sK16,sK17,sK17) | sK17 = sK3(sK16,sK17,sK17) | ~spl19_32),
% 0.20/0.32 inference(resolution,[],[f698,f1041])).
% 0.20/0.32 tff(f2262,plain,(
% 0.20/0.32 sK17 = sK3(sK16,sK17,sK17) | (spl19_8 | ~spl19_9 | ~spl19_32)),
% 0.20/0.32 inference(forward_subsumption_resolution,[],[f2258,f966])).
% 0.20/0.32 tff(f2264,plain,(
% 0.20/0.32 ~repr1(sK16,sK17,sK17) | same1(sK16,sK17,sK17) | ~repr1(sK16,sK17,sK17) | (spl19_8 | ~spl19_9 | ~spl19_32)),
% 0.20/0.32 inference(superposition,[],[f111,f2262])).
% 0.20/0.32 tff(f2270,plain,(
% 0.20/0.32 ~repr1(sK16,sK17,sK17) | same1(sK16,sK17,sK17) | (spl19_8 | ~spl19_9 | ~spl19_32)),
% 0.20/0.32 inference(duplicate_literal_removal,[],[f2264])).
% 0.20/0.32 tff(f2271,plain,(
% 0.20/0.32 same1(sK16,sK17,sK17) | (~spl19_1 | ~spl19_3 | spl19_5 | spl19_8 | ~spl19_9 | ~spl19_32)),
% 0.20/0.32 inference(forward_subsumption_resolution,[],[f2270,f972])).
% 0.20/0.32 tff(f2272,plain,(
% 0.20/0.32 $false | (~spl19_1 | ~spl19_3 | spl19_5 | spl19_8 | ~spl19_9 | ~spl19_32)),
% 0.20/0.32 inference(forward_subsumption_resolution,[],[f2271,f966])).
% 0.20/0.32 tff(f2273,plain,(
% 0.20/0.32 ~spl19_1 | ~spl19_3 | spl19_5 | spl19_8 | ~spl19_9 | ~spl19_32),
% 0.20/0.32 inference(avatar_contradiction_clause,[],[f2272])).
% 0.20/0.32 tff(f2288,plain,(
% 0.20/0.32 ~$less(sK18,size1(sK16)) | sK17 = sK18 | ~$less(sK17,size1(sK16)) | $less(sK18,0) | $less(sK17,0) | (~spl19_3 | ~spl19_8)),
% 0.20/0.32 inference(resolution,[],[f198,f223])).
% 0.20/0.32 tff(f2291,plain,(
% 0.20/0.32 ~$less(sK18,size1(sK16)) | sK17 = sK18 | $less(sK18,0) | $less(sK17,0) | (~spl19_1 | ~spl19_3 | ~spl19_8)),
% 0.20/0.32 inference(forward_subsumption_resolution,[],[f2288,f903])).
% 0.20/0.32 tff(f2293,plain,(
% 0.20/0.32 ~$less(sK18,size1(sK16)) | sK17 = sK18 | $less(sK17,0) | (~spl19_1 | ~spl19_3 | spl19_7 | ~spl19_8)),
% 0.20/0.32 inference(forward_subsumption_resolution,[],[f2291,f193])).
% 0.20/0.32 tff(f2295,plain,(
% 0.20/0.32 ~$less(sK18,size1(sK16)) | sK17 = sK18 | (~spl19_1 | ~spl19_3 | spl19_5 | spl19_7 | ~spl19_8)),
% 0.20/0.32 inference(forward_subsumption_resolution,[],[f2293,f183])).
% 0.20/0.32 tff(f2298,definition,(
% 0.20/0.32 spl19_37 <=> sK17 = sK18),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_37])],[avatar_definition])).
% 0.20/0.32 tff(f2300,plain,(
% 0.20/0.32 sK17 = sK18 | ~spl19_37),
% 0.20/0.32 inference(avatar_component_clause,[],[f2298])).
% 0.20/0.32 tff(f2302,definition,(
% 0.20/0.32 spl19_38 <=> $less(sK18,size1(sK16))),
% 0.20/0.32 introduced(definition,[new_symbols(definition,[spl19_38])],[avatar_definition])).
% 0.20/0.32 tff(f2305,plain,(
% 0.20/0.32 spl19_37 | ~spl19_38 | ~spl19_1 | ~spl19_3 | spl19_5 | spl19_7 | ~spl19_8),
% 0.20/0.32 inference(avatar_split_clause,[],[f2295,f196,f191,f181,f172,f164,f2302,f2298])).
% 0.20/0.32 tff(f2311,plain,(
% 0.20/0.32 spl19_38 | ~spl19_3 | ~spl19_6),
% 0.20/0.32 inference(avatar_split_clause,[],[f904,f186,f172,f2302])).
% 0.20/0.32 tff(f2312,plain,(
% 0.20/0.32 ~path1(sK15,sK17,sK17) | (spl19_9 | ~spl19_37)),
% 0.20/0.32 inference(superposition,[],[f201,f2300])).
% 0.20/0.32 tff(f2317,plain,(
% 0.20/0.32 $false | (spl19_9 | ~spl19_37)),
% 0.20/0.32 inference(forward_subsumption_resolution,[],[f2312,f156])).
% 0.20/0.32 tff(f2318,plain,(
% 0.20/0.32 spl19_9 | ~spl19_37),
% 0.20/0.32 inference(avatar_contradiction_clause,[],[f2317])).
% 0.20/0.32 cnf(s1, plain, spl19_1 | ~spl19_2 | ~spl19_3 | spl19_4, inference(sat_conversion,[],[f179])).
% 0.20/0.32 cnf(s2, plain, ~spl19_2 | ~spl19_3 | spl19_4 | ~spl19_5, inference(sat_conversion,[],[f184])).
% 0.20/0.32 cnf(s3, plain, ~spl19_2 | ~spl19_3 | spl19_4 | spl19_6, inference(sat_conversion,[],[f189])).
% 0.20/0.32 cnf(s4, plain, ~spl19_2 | ~spl19_3 | spl19_4 | ~spl19_7, inference(sat_conversion,[],[f194])).
% 0.20/0.32 cnf(s5, plain, ~spl19_2 | ~spl19_3 | spl19_4 | spl19_8 | spl19_9, inference(sat_conversion,[],[f203])).
% 0.20/0.32 cnf(s6, plain, ~spl19_2 | ~spl19_3 | spl19_4 | ~spl19_8 | ~spl19_9, inference(sat_conversion,[],[f204])).
% 0.20/0.32 cnf(s7, plain, spl19_2, inference(sat_conversion,[],[f205])).
% 0.20/0.32 cnf(s10, plain, ~spl19_2 | spl19_3, inference(sat_conversion,[],[f214])).
% 0.20/0.32 cnf(s14, plain, spl19_10 | spl19_11, inference(sat_conversion,[],[f312])).
% 0.20/0.32 cnf(s20, plain, ~spl19_4 | ~spl19_10, inference(sat_conversion,[],[f370])).
% 0.20/0.32 cnf(s30, plain, ~spl19_3 | spl19_14 | spl19_18, inference(sat_conversion,[],[f627])).
% 0.20/0.32 cnf(s39, plain, ~spl19_11 | ~spl19_14, inference(sat_conversion,[],[f705])).
% 0.20/0.32 cnf(s43, plain, ~spl19_3 | ~spl19_4 | ~spl19_11 | ~spl19_18, inference(sat_conversion,[],[f897])).
% 0.20/0.32 cnf(s52, plain, ~spl19_1 | ~spl19_3 | spl19_5 | spl19_32, inference(sat_conversion,[],[f1078])).
% 0.20/0.32 cnf(s53, plain, ~spl19_1 | ~spl19_3 | spl19_5 | spl19_8 | ~spl19_9 | ~spl19_32, inference(sat_conversion,[],[f2273])).
% 0.20/0.32 cnf(s56, plain, ~spl19_1 | ~spl19_3 | spl19_5 | spl19_7 | ~spl19_8 | spl19_37 | ~spl19_38, inference(sat_conversion,[],[f2305])).
% 0.20/0.32 cnf(s58, plain, ~spl19_3 | ~spl19_6 | spl19_38, inference(sat_conversion,[],[f2311])).
% 0.20/0.32 cnf(s60, plain, spl19_9 | ~spl19_37, inference(sat_conversion,[],[f2318])).
% 0.20/0.32 cnf(s66, plain, spl19_3, inference(rat,[],[s10,s7])).
% 0.20/0.32 cnf(s67, plain, spl19_4 | ~spl19_8 | ~spl19_9, inference(rat,[],[s6,s66,s7])).
% 0.20/0.32 cnf(s68, plain, spl19_4 | spl19_8 | spl19_9, inference(rat,[],[s5,s66,s7])).
% 0.20/0.32 cnf(s69, plain, spl19_4 | ~spl19_7, inference(rat,[],[s4,s66,s7])).
% 0.20/0.32 cnf(s70, plain, spl19_4 | spl19_6, inference(rat,[],[s3,s66,s7])).
% 0.20/0.32 cnf(s71, plain, spl19_4 | ~spl19_5, inference(rat,[],[s2,s66,s7])).
% 0.20/0.32 cnf(s72, plain, spl19_1 | spl19_4, inference(rat,[],[s1,s66,s7])).
% 0.20/0.32 cnf(s73, plain, ~spl19_4, inference(rat,[],[s30,s43,s39,s14,s20,s66])).
% 0.20/0.32 cnf(s74, plain, ~spl19_7, inference(rat,[],[s69,s73])).
% 0.20/0.32 cnf(s75, plain, spl19_6, inference(rat,[],[s70,s73])).
% 0.20/0.32 cnf(s76, plain, ~spl19_5, inference(rat,[],[s71,s73])).
% 0.20/0.32 cnf(s77, plain, spl19_1, inference(rat,[],[s72,s73])).
% 0.20/0.32 cnf(s78, plain, spl19_38, inference(rat,[],[s58,s66,s75])).
% 0.20/0.32 cnf(s79, plain, spl19_32, inference(rat,[],[s52,s77,s66,s76])).
% 0.20/0.32 cnf(s80, plain, spl19_8, inference(rat,[],[s53,s68,s66,s76,s77,s79,s73])).
% 0.20/0.32 cnf(s81, plain, ~spl19_9, inference(rat,[],[s67,s73,s80])).
% 0.20/0.32 cnf(s83, plain, spl19_37, inference(rat,[],[s56,s78,s76,s74,s77,s66,s80])).
% 0.20/0.32 cnf(s84, plain, $false, inference(rat,[],[s60,s83,s81])).
% 0.20/0.32 tff(f2319,plain,(
% 0.20/0.32 $false),
% 0.20/0.32 inference(avatar_sat_refutation,[],[s84])).
% 0.20/0.32 % SZS output end Proof for theBenchmark
% 0.20/0.32 % (1955660)------------------------------
% 0.20/0.32 % (1955660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.32 % (1955660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.32 % (1955660)CaDiCaL version: 2.1.3
% 0.20/0.32 % (1955660)Termination reason: Refutation
% 0.20/0.32 % (1955660)Time elapsed: 0.037 s
% 0.20/0.32 % (1955660)Peak memory usage: 14 MB
% 0.20/0.32 % (1955660)Instructions burned: 101 (million)
% 0.20/0.32 % (1955641)Success in time 0.08 s
% 0.20/0.32 % Vampire exiting
%------------------------------------------------------------------------------