%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX220+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 29 02:38:07 PM UTC 2026 % Result : Theorem 13.92s 14.22s % Output : Refutation 13.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX220+1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.15/0.33 % Computer : n007.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Wed Apr 29 01:58:38 EDT 2026 % 0.15/0.33 % CPUTime : % 0.42/1.00 ============================== Prover9 =============================== % 0.42/1.00 Prover9 (32) version 2009-11A, November 2009. % 0.42/1.00 Process 13082 was started by sandbox on n007.cluster.edu, % 0.42/1.00 Wed Apr 29 01:58:39 2026 % 0.42/1.00 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_12929_n007.cluster.edu". % 0.42/1.00 ============================== end of head =========================== % 0.42/1.00 % 0.42/1.00 ============================== INPUT ================================= % 0.42/1.00 % 0.42/1.00 % Reading from file /tmp/Prover9_12929_n007.cluster.edu % 0.42/1.00 % 0.42/1.00 set(prolog_style_variables). % 0.42/1.00 set(auto2). % 0.42/1.00 % set(auto2) -> set(auto). % 0.42/1.00 % set(auto) -> set(auto_inference). % 0.42/1.00 % set(auto) -> set(auto_setup). % 0.42/1.00 % set(auto_setup) -> set(predicate_elim). % 0.42/1.00 % set(auto_setup) -> assign(eq_defs, unfold). % 0.42/1.00 % set(auto) -> set(auto_limits). % 0.42/1.00 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.42/1.00 % set(auto_limits) -> assign(sos_limit, 20000). % 0.42/1.00 % set(auto) -> set(auto_denials). % 0.42/1.00 % set(auto) -> set(auto_process). % 0.42/1.00 % set(auto2) -> assign(new_constants, 1). % 0.42/1.00 % set(auto2) -> assign(fold_denial_max, 3). % 0.42/1.00 % set(auto2) -> assign(max_weight, "200.000"). % 0.42/1.00 % set(auto2) -> assign(max_hours, 1). % 0.42/1.00 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.42/1.00 % set(auto2) -> assign(max_seconds, 0). % 0.42/1.00 % set(auto2) -> assign(max_minutes, 5). % 0.42/1.00 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.42/1.00 % set(auto2) -> set(sort_initial_sos). % 0.42/1.00 % set(auto2) -> assign(sos_limit, -1). % 0.42/1.00 % set(auto2) -> assign(lrs_ticks, 3000). % 0.42/1.00 % set(auto2) -> assign(max_megs, 400). % 0.42/1.00 % set(auto2) -> assign(stats, some). % 0.42/1.00 % set(auto2) -> clear(echo_input). % 0.42/1.00 % set(auto2) -> set(quiet). % 0.42/1.00 % set(auto2) -> clear(print_initial_clauses). % 0.42/1.00 % set(auto2) -> clear(print_given). % 0.42/1.00 assign(lrs_ticks,-1). % 0.42/1.00 assign(sos_limit,10000). % 0.42/1.00 assign(order,kbo). % 0.42/1.00 set(lex_order_vars). % 0.42/1.00 clear(print_given). % 0.42/1.00 % 0.42/1.00 % formulas(sos). % not echoed (32 formulas) % 0.42/1.00 % 0.42/1.00 ============================== end of input ========================== % 0.42/1.00 % 0.42/1.00 % From the command line: assign(max_seconds, 300). % 0.42/1.00 % 0.42/1.00 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.42/1.00 % 0.42/1.00 % Formulas that are not ordinary clauses: % 0.42/1.00 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 2 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 4 (all X all X2 proj1Arr(arr(X,X2)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 5 (all X all X2 proj2Arr(arr(X,X2)) = X2) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 6 (all X all X2 arr(X,X2) != a) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 7 (all X all X2 arr(X,X2) != b) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 8 (all X all X2 arr(X,X2) != c) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 9 (all X proj1Suc(suc(X)) = X) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 10 (all X zero != suc(X)) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 11 (all X proj1Just(just(X)) = X) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 12 (all X nothing != just(X)) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 13 (all X all X2 all X3 proj1App(app(X,X2,X3)) = X) # label(axiom_016) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 14 (all X all X2 all X3 proj2App(app(X,X2,X3)) = X2) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 15 (all X all X2 all X3 proj3App(app(X,X2,X3)) = X3) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 16 (all X proj1Lam(lam(X)) = X) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 17 (all X proj1Var(var(X)) = X) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 18 (all X all X2 all X3 all X4 app(X,X2,X3) != lam(X4)) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 19 (all X al % 0.42/1.00 WARNING: denials share constants (see output). % 0.42/1.00 % 1.32/1.68 l X2 all X3 all X4 app(X,X2,X3) != var(X4)) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 1.32/1.68 20 (all X all X2 lam(X) != var(X2)) # label(axiom_023) # label(axiom) # label(non_clause). [assumption]. % 1.32/1.68 21 (all Y index(nil,Y) = nothing) # label(axiom_024) # label(axiom) # label(non_clause). [assumption]. % 1.32/1.68 22 (all Z all Xs index(cons(Z,Xs),zero) = just(Z)) # label(axiom_025) # label(axiom) # label(non_clause). [assumption]. % 1.32/1.68 23 (all Z all Xs all N index(cons(Z,Xs),suc(N)) = index(Xs,N)) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 1.32/1.68 24 (all X all Z all F all X2 all Tx (tc(X,app(F,X2,Tx),Z) <-> tc(X,F,arr(Tx,Z)) & tc(X,X2,Tx))) # label(axiom_027) # label(axiom) # label(non_clause). [assumption]. % 1.32/1.68 25 (all X all Z all E (Z != arr(proj1Arr(Z),proj2Arr(Z)) -> -tc(X,lam(E),Z))) # label(axiom_028) # label(axiom) # label(non_clause). [assumption]. % 1.32/1.68 26 (all X all E all Tx2 all T1 (tc(X,lam(E),arr(Tx2,T1)) <-> tc(cons(Tx2,X),E,T1))) # label(axiom_029) # label(axiom) # label(non_clause). [assumption]. % 1.32/1.68 27 (all X all Z all X3 (index(X,X3) = nothing -> -tc(X,var(X3),Z))) # label(axiom_030) # label(axiom) # label(non_clause). [assumption]. % 1.32/1.68 28 (all X all Z all X3 all Tx3 (index(X,X3) = just(Tx3) -> (tc(X,var(X3),Z) <-> Tx3 = Z))) # label(axiom_031) # label(axiom) # label(non_clause). [assumption]. % 1.32/1.68 29 -(exists E tc(nil,E,arr(arr(a,arr(b,c)),arr(b,arr(a,c))))) # label(goal_032) # label(negated_conjecture) # label(non_clause). [assumption]. % 1.32/1.68 % 1.32/1.68 ============================== end of process non-clausal formulas === % 1.32/1.68 % 1.32/1.68 ============================== PROCESS INITIAL CLAUSES =============== % 1.32/1.68 % 1.32/1.68 ============================== PREDICATE ELIMINATION ================= % 1.32/1.68 % 1.32/1.68 ============================== end predicate elimination ============= % 1.32/1.68 % 1.32/1.68 Auto_denials: % 1.32/1.68 % copying label axiom_009 to answer in negative clause % 1.32/1.68 % copying label axiom_010 to answer in negative clause % 1.32/1.68 % copying label axiom_011 to answer in negative clause % 1.32/1.68 % copying label axiom_013 to answer in negative clause % 1.32/1.68 % copying label axiom_015 to answer in negative clause % 1.32/1.68 % copying label axiom_003 to answer in negative clause % 1.32/1.68 % copying label axiom_006 to answer in negative clause % 1.32/1.68 % copying label axiom_007 to answer in negative clause % 1.32/1.68 % copying label axiom_008 to answer in negative clause % 1.32/1.68 % copying label axiom_023 to answer in negative clause % 1.32/1.68 % copying label axiom_021 to answer in negative clause % 1.32/1.68 % copying label axiom_022 to answer in negative clause % 1.32/1.68 % copying label axiom_030 to answer in negative clause % 1.32/1.68 % copying label goal_032 to answer in negative clause % 1.32/1.68 % assign(max_proofs, 14). % (Horn set with more than one neg. clause) % 1.32/1.68 % 1.32/1.68 WARNING, because some of the denials share constants, % 1.32/1.68 some of the denials or their descendents may be subsumed, % 1.32/1.68 preventing the target number of proofs from being found. % 1.32/1.68 The shared constants are: nil, nothing, c, b, a. % 1.32/1.68 % 1.32/1.68 Term ordering decisions: % 1.32/1.68 Function symbol KB weights: nil=1. nothing=1. zero=1. a=1. b=1. c=1. arr=1. cons=1. index=1. just=1. lam=1. var=1. proj1Arr=1. proj2Arr=1. suc=1. head=1. proj1App=1. proj1Just=1. proj1Lam=1. proj1Suc=1. proj1Var=1. proj2App=1. proj3App=1. tail=1. app=1. % 1.32/1.68 % 1.32/1.68 ============================== end of process initial clauses ======== % 1.32/1.68 % 1.32/1.68 ============================== CLAUSES FOR SEARCH ==================== % 1.32/1.68 % 1.32/1.68 ============================== end of clauses for search ============= % 1.32/1.68 % 1.32/1.68 ============================== SEARCH ================================ % 1.32/1.68 % 1.32/1.68 % Starting search at 0.02 seconds. % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=60.000, iters=3429 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=59.000, iters=3421 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=50.000, iters=3369 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=49.000, iters=3352 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=46.000, iters=3391 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=45.000, iters=3336 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=42.000, iters=3398 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=41.000, iters=3337 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=40.000, iters=3373 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=39.000, iters=3485 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=38.000, iters=3377 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=37.000, iters=3334 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=36.000, iters=3430 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=35.000, iters=3348 % 1.32/1.68 % 1.32/1.68 Low Water (keep): wt=34.000, iters=3355 % 13.92/14.22 % 13.92/14.22 Low Water (keep): wt=33.000, iters=3380 % 13.92/14.22 % 13.92/14.22 Low Water (keep): wt=32.000, iters=3418 % 13.92/14.22 % 13.92/14.22 Low Water (keep): wt=31.000, iters=3335 % 13.92/14.22 % 13.92/14.22 Low Water (keep): wt=30.000, iters=3336 % 13.92/14.22 % 13.92/14.22 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 275 (0.00 of 2.73 sec). % 13.92/14.22 % 13.92/14.22 Low Water (keep): wt=29.000, iters=3335 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=3339, wt=76.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=3351, wt=75.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=3535, wt=69.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=3330, wt=68.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=3342, wt=65.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=3356, wt=64.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=9543, wt=34.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=10669, wt=32.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=10670, wt=30.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=10671, wt=28.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=10551, wt=26.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=7849, wt=25.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=11049, wt=24.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=11243, wt=22.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=11247, wt=20.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=11798, wt=18.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=12493, wt=16.000 % 13.92/14.22 % 13.92/14.22 Low Water (displace): id=12495, wt=15.000 % 13.92/14.22 % 13.92/14.22 ============================== PROOF ================================= % 13.92/14.22 % SZS status Theorem % 13.92/14.22 % SZS output start Refutation % 13.92/14.22 % 13.92/14.22 % Proof 1 at 13.01 (+ 0.23) seconds: goal_032. % 13.92/14.22 % Length of proof is 25. % 13.92/14.22 % Level of proof is 7. % 13.92/14.22 % Maximum clause weight is 26.000. % 13.92/14.22 % Given clauses 1144. % 13.92/14.22 % 13.92/14.22 15 (all X all X2 all X3 proj3App(app(X,X2,X3)) = X3) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 13.92/14.22 22 (all Z all Xs index(cons(Z,Xs),zero) = just(Z)) # label(axiom_025) # label(axiom) # label(non_clause). [assumption]. % 13.92/14.22 23 (all Z all Xs all N index(cons(Z,Xs),suc(N)) = index(Xs,N)) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 13.92/14.22 24 (all X all Z all F all X2 all Tx (tc(X,app(F,X2,Tx),Z) <-> tc(X,F,arr(Tx,Z)) & tc(X,X2,Tx))) # label(axiom_027) # label(axiom) # label(non_clause). [assumption]. % 13.92/14.22 26 (all X all E all Tx2 all T1 (tc(X,lam(E),arr(Tx2,T1)) <-> tc(cons(Tx2,X),E,T1))) # label(axiom_029) # label(axiom) # label(non_clause). [assumption]. % 13.92/14.22 28 (all X all Z all X3 all Tx3 (index(X,X3) = just(Tx3) -> (tc(X,var(X3),Z) <-> Tx3 = Z))) # label(axiom_031) # label(axiom) # label(non_clause). [assumption]. % 13.92/14.22 29 -(exists E tc(nil,E,arr(arr(a,arr(b,c)),arr(b,arr(a,c))))) # label(goal_032) # label(negated_conjecture) # label(non_clause). [assumption]. % 13.92/14.22 41 proj3App(app(A,B,C)) = C # label(axiom_018) # label(axiom). [clausify(15)]. % 13.92/14.22 42 index(cons(A,B),zero) = just(A) # label(axiom_025) # label(axiom). [clausify(22)]. % 13.92/14.22 43 index(cons(A,B),suc(C)) = index(B,C) # label(axiom_026) # label(axiom). [clausify(23)]. % 13.92/14.22 60 -tc(nil,A,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))) # label(goal_032) # label(negated_conjecture) # answer(goal_032). [clausify(29)]. % 13.92/14.22 65 tc(A,lam(B),arr(C,D)) | -tc(cons(C,A),B,D) # label(axiom_029) # label(axiom). [clausify(26)]. % 13.92/14.22 67 index(A,B) != just(C) | tc(A,var(B),D) | C != D # label(axiom_031) # label(axiom). [clausify(28)]. % 13.92/14.22 68 tc(A,app(B,C,D),E) | -tc(A,B,arr(D,E)) | -tc(A,C,D) # label(axiom_027) # label(axiom). [clausify(24)]. % 13.92/14.22 75 -tc(cons(arr(a,arr(b,c)),nil),A,arr(b,arr(a,c))) # answer(goal_032). [ur(65,a,60,a)]. % 13.92/14.22 102 tc(cons(A,B),var(zero),A). [hyper(67,a,42,a,c,41,a),rewrite([41(2)])]. % 13.92/14.22 104 index(A,B) != just(C) | tc(cons(D,A),var(suc(B)),E) | C != E. [para(43(a,1),67(a,1))]. % 13.92/14.22 290 -tc(cons(b,cons(arr(a,arr(b,c)),nil)),A,arr(a,c)) # answer(goal_032). [ur(65,a,75,a)]. % 13.92/14.22 305 tc(cons(A,cons(B,C)),var(suc(zero)),B). [hyper(104,a,42,a,c,41,a),rewrite([41(2)])]. % 13.92/14.22 307 index(A,B) != just(C) | tc(cons(D,cons(E,A)),var(suc(suc(B))),F) | C != F. [para(43(a,1),104(a,1))]. % 13.92/14.22 5234 tc(cons(A,cons(B,cons(C,D))),var(suc(suc(zero))),C). [hyper(307,a,42,a,c,41,a),rewrite([41(2)])]. % 13.92/14.22 5352 tc(cons(A,cons(B,cons(arr(A,C),D))),app(var(suc(suc(zero))),var(zero),A),C). [hyper(68,b,5234,a,c,102,a)]. % 13.92/14.22 6333 tc(cons(A,cons(B,cons(arr(A,arr(B,C)),D))),app(app(var(suc(suc(zero))),var(zero),A),var(suc(zero)),B),C). [hyper(68,b,5352,a,c,305,a)]. % 13.92/14.22 13320 -tc(cons(a,cons(b,cons(arr(a,arr(b,c)),nil))),A,c) # answer(goal_032). [ur(65,a,290,a)]. % 13.92/14.22 13321 $F # answer(goal_032). [resolve(13320,a,6333,a)]. % 13.92/14.25 % 13.92/14.25 % SZS output end Refutation % 13.92/14.25 ============================== end of proof ========================== % 13.92/14.25 % Redundant proof: 13322 $F # answer(goal_032). [resolve(13320,a,6332,a)]. % 13.92/14.25 % 13.92/14.25 % Disable descendants (x means already disabled): % 13.92/14.25 60 70 74x 75 132 139 145 146 181 196x % 13.92/14.25 197x 283 284 285 286 287 288 289 290 291x % 13.92/14.25 292 355 384 385 386 387 525x 526x 903x 904x % 13.92/14.25 1094x 1564 1565 1566 1567 1568 1569 1570 1571 1572 % 13.92/14.25 1573 1574 1575 1576 1577 1578 1579 1580 1581 1812 % 13.92/14.25 1813 1814 1815 1816 1817 1818 1819 1820 1821 1822 % 13.92/14.25 1823 1824 1825 1826 1827 1828 1829 1830 1831 1832 % 13.92/14.25 1833 1834 1835 1836 1837 1838 1839 1840 1841 1842 % 13.92/14.25 1843 1844 2100 2101 2102 2103 2104 2105x 2106x 2109 % 13.92/14.25 2110 2111 2112 2113 2114 2115 2116 2117 2118 2119 % 13.92/14.25 2120 2121 2122 2123 2124 2125 2126 2127 2128 2129 % 13.92/14.25 2130 2131 2132 2133 2134 2135 2136 2137 2138 2139 % 13.92/14.25 2140 2141 2142 2143 2144 2145 2456 2457 2458 2459 % 13.92/14.25 2460 2461 2462 2463 2464 2465 2466 2467 2468 2469 % 13.92/14.25 2470 2471 2472 2473 2474 2475 2476 2477 2478 2479 % 13.92/14.25 2480 2481 2482 2483 2484 2485 2486 2487 2488 2795 % 13.92/14.25 2796 2797 2798 2799 2800 2801 2802 2803 2804 2805x % 13.92/14.25 2806x 2916x 2917 2918 2919 2920x 2921 2922x 2923 2924 % 13.92/14.25 2925 2926 2927 2928 2929x 2930 2931 2932 2933 2934 % 13.92/14.25 2935 2936 2937 2938 2939 2940 2941 2942 2943x 2944 % 13.92/14.25 2945 2946 2947 2948 2949 2950 2951 2952 2953 2954 % 13.92/14.25 2955 2956 4039 4192x 4193x 4194x 4195x 4196x 4197x 4198x % 13.92/14.25 4199x 4200x 4201 4202 4428 4429 4430 4431 4432 4433 % 13.92/14.25 4434 4435 4436 4437 4438 4439 4440 4441x 4442x 4443x % 13.92/14.25 5064x 5065x 5066x 5067x 5068x 5069x 5070x 5071x 5072x 5073 % 13.92/14.25 5074x 5619 5620 5621 5622 5623 5624 5625 5626 5627x % 13.92/14.25 5634 5635 5636 5637 5638 5784 5785 5786 5787 5788 % 13.92/14.25 5789 5790 5791 5792 5793 5794 5795 5796 5797x 5798x % 13.92/14.25 5799x 5800x 5801 5963x 5964x 5965 5966 5967 5968 5969 % 13.92/14.25 5970 6212x 6213x 6407 6408 6409 6410 6411 6412 6413 % 13.92/14.25 6414 6415 6416 6417 6418 6419 6420x 6421x 6422x 6423x % 13.92/14.25 6607 6608 6609 6610 6611 6612 6613 6614 6615 6616 % 13.92/14.25 6617 6618 6619 6684 6685 6686 6687 6688 6689 6690 % 13.92/14.25 6691 6692 6693 6694 6695 6696 6697 6698 6699 6700 % 13.92/14.25 6701 6702 6703 6704 6705 6706 6707 6708 6709 6710 % 13.92/14.25 6711 6712 6713 6714 6715 6716 6717 6718 6719 6720 % 13.92/14.25 6721 6722 6723 6724 6725 6726 6727 6728 6729 6730 % 13.92/14.25 6731 6732 6733 6734 6735 6736 6737 6738 6739 6740 % 13.92/14.25 6741 6742 6743 6744 6745 6746 6747 6781 6782 6783 % 13.92/14.25 6784 6785 6786 6787 6788x 6789x 6790x 6791 6792x 6793 % 13.92/14.25 6794 6795x 6796 6797 6798 6799x 6800x 6801x 6802x 6836 % 13.92/14.25 6837 6838 6839 6840 6841 6842 6843 6844 6845 6846 % 13.92/14.25 6847 6848 6849 6850 6851x 6852 6853 6854 6855 6856 % 13.92/14.25 6857 6858 6859 6860 6861 6862 6939 6940 6941 6942 % 13.92/14.25 6943 6944 6945 6946 6947 6948 6949 6950 6951x 6952 % 13.92/14.25 6953 6954 6955 6956 6957 6958 6959 6960 6961 6962 % 13.92/14.25 6963 6964 6965 6966 6967 6968 6969 6970 6971x 6972 % 13.92/14.25 6973 6974 6975 6976 6977 6978 6979 6980 6981 6982 % 13.92/14.25 6983 6984 6985 6986 6987 6988 6989 6990 6991 6992 % 13.92/14.25 6993x 6994 6995 6996 6997 6998 6999 7049 7050 7051 % 13.92/14.25 7055 7056 7057 7058 7059 7060 7061 7062 7063 7064 % 13.92/14.25 7065 7066 7067 7068 7069 7070 7071 7072x 7073 7074 % 13.92/14.25 7075 7076 7077 7078 7079 7132 7133 7134 7135 7136 % 13.92/14.25 7137 7138 7139 7140 7141 7142 7143 7144 7145 7146x % 13.92/14.25 7147 7148 7149 7150 7151 7152 7153 7154 7155 7156 % 13.92/14.25 7157 7158 7159 7160 7161 7162 7163 7164 7165 7166 % 13.92/14.25 7167 7168 7169x 7170 7171 7172 7173 7174 7175 7176 % 13.92/14.25 7177 7178 7228 7229 7230 7237 7238 7239 7310 7311 % 13.92/14.25 7312 7313 7314 7315 7316 7317 7318 7319 7320 7321 % 13.92/14.25 7322x 7323 7324 7325 7326 7327 7328 7329 7330 7331 % 13.92/14.25 7332 7333 7334 7335 7336 7337 7338 7339 7340 7341 % 13.92/14.25 7342 7343 7344x 7345 7346 7347 7348 7349 7350 7351 % 13.92/14.25 7352 7353 7466 7467 7468 7637 7638 7688 7689 7690 % 13.92/14.25 7691 7692 7693 7694 7695 7696 7697 7698 7699 7700x % 13.92/14.25 7701 7702 7703 7704 7705 7706 7707 7708 7709 7710 % 13.92/14.25 7711 7712x 7713 7714x 7715 7716 7717 7718 7719 7720 % 13.92/14.25 7721 7722 7723x 7724 7725 7726 7727 7728 7766 7767 % 13.92/14.25 7768 7769 7770 7771x 7772 7773x 7774 7775 7776 7777 % 13.92/14.25 7778 7779 7780 7781 7782x 7783 7784 7785 7786 7787 % 13.92/14.25 7788x 7789 7790x 7791 7792x 7793 7794 7795 7796 7797 % 13.92/14.25 7798 7799 7800x 7801 7802 7803 7804 7805 7836x 7837x % 13.92/14.25 7838x 7839x 7840x 7841x 7842x 7843x 7844x 7845x 7846x 7847x % 13.92/14.25 7848x 7849x 7850x 7851 7852x 7853 7854 7855 7856 7857 % 13.92/14.25 7858 7859 7860 7861 7862 7863 7864x 7865 7866 7867 % 13.92/14.25 7868 7869 7870 7871 7872 7873 7874x 7875 7876 7877 % 13.92/14.25 7878 7879 7880 7881 7882 7883 7884x 7885 7886 7887 % 13.92/14.25 7888 7889 7890 7891 7892 7893 7894 7895 7896 7897 % 13.92/14.25 7898 7899 7900 7901 7902 7903x 7904 7905 7906 7907 % 13.92/14.25 7908 7909x 7910 7911x 7912 7913 7914 7915 7916 7917 % 13.92/14.25 7918 7919 7920 7921 7922 7923x 7924 7925 7926 7927 % 13.92/14.25 7958 7959 7960 7961 7962 7963x 7964 7965 7966 7967 % 13.92/14.25 7968 7969 7970 7971 7972 7973x 7974 7975 7976 7977 % 13.92/14.25 7978 7979 7980 7981 7982 7983 7984 7985 7986 7987 % 13.92/14.25 7988 7989 7990 7991 7992 7993x 7994 7995 7996 7997 % 13.92/14.25 7998 7999 8000 8001 8002 8003 8004 8005 8006 8007 % 13.92/14.25 8008 8009 8010 8011 8012 8013x 8014 8015 8016 8017 % 13.92/14.25 8018 8019 8020 8021 8022 8023 8024 8025 8026 8027 % 13.92/14.25 8028 8029 8030 8031 8032x 8033 8034 8035 8036 8078 % 13.92/14.25 8079 8080 8081 8082 8083 8084 8085 8086 8087 8088 % 13.92/14.25 8089 8090 8091x 8092 8093 8094 8095 8096 8097 8098 % 13.92/14.25 8099x 8100 8101 8102x 8103 8104 8105 8106 8107 8108 % 13.92/14.25 8109 8110x 8111 8112 8113 8114 8115 8116 8117 8118 % 13.92/14.25 8119 8120 8121 8122 8123 8124 8125 8126 8127 8128 % 13.92/14.25 8129 8130 8131x 8132 8133 8134 8135 8136 8137 8138 % 13.92/14.25 8209x 8210x 8211x 8212x 8213x 8214x 8215x 8216x 8217x 8218x % 13.92/14.25 8219x 8220x 8221x 8222x 8223x 8224x 8225x 8226 8227x 8228x % 13.92/14.25 8229x 8230 8231x 8232 8233 8234x 8235x 8236 8237 8238x % 13.92/14.25 8239 8240x 8241x 8242x 8243 8244x 8245 8246 8247x 8248 % 13.92/14.25 8249 8250 8251x 8252x 8253x 8254x 8255x 8310 8311 8312 % 13.92/14.25 8313 8314 8315 8316 8317 8318 8319 8320 8321 8322 % 13.92/14.25 8323 8324 8325 8326 8327 8328 8329 8330 8331 8332 % 13.92/14.25 8333 8334 8335 8336 8337 8338 8339 8340 8341 8342 % 13.92/14.25 8343 8344 8345 8346 8347 8348 8349 8350 8351 8352x % 13.92/14.25 8353x 8354x 8355x 8356x 8835 8836 8848 8849 8850 8851 % 13.92/14.25 8852 8853 8854 8855 8856 8857 8858 8859x 8860x 8861 % 13.92/14.25 8862x 8863 8864 8865 8866 8867 8868 8869 8870 8871 % 13.92/14.25 8872 8873 8874 8875 8876 8877 8878 8879 8880 8881 % 13.92/14.25 8882 8883x 8908 8909 8910 8911 8912 8913 8914 8915 % 13.92/14.25 8916 8917 8918 8939 8940 8941 8942 8943 8944 8945 % 13.92/14.25 8946 8947 8948 8949 8950 9149 9150 9151 9152 9168 % 13.92/14.25 9169 9170 9171 9172 9194 9195 9196 9197 9198 9199 % 13.92/14.25 9236 9237 9238 9239 9240 9241 9242 9243 9244 9245 % 13.92/14.25 9246 9247 9248 9249 9250 9251 9252 9253 9254 9255 % 13.92/14.25 9256 9257 9258 9259 9260 9261 9262 9263 9264 9265 % 13.92/14.25 9266 9267 9268 9269 9270 9271 9272 9273 9274 9275 % 13.92/14.25 9276 9277 9278x 9279x 9280x 9281x 9282x 9350 9351 9352 % 13.92/14.25 9353 9354 9355 9356 9357 9358 9384 9385 9386 9387 % 13.92/14.25 9388 9389 9390 9391 9392 9393 9394 9395x 9396 9397 % 13.92/14.25 9398x 9399 9400 9401x 9402 9403x 9404x 9405x 9406x 9407x % 13.92/14.25 9408 9409 9410x 9411x 9412 9413 9414 9415 9416 9417 % 13.92/14.25 9442 9443 9444 9500x 9501x 9502x 9503x 9504x 9505x 9506x % 13.92/14.25 9507x 9508x 9509x 9510x 9511x 9512x 9513x 9514x 9515x 9516x % 13.92/14.25 9517 9518x 9519x 9520x 9521 9522x 9523 9524 9525x 9526x % 13.92/14.25 9527 9528 9529x 9530 9531x 9532x 9533x 9534 9535x 9536 % 13.92/14.25 9537 9538x 9539 9540 9541 9542x 9543x 9544x 9545x 9546x % 13.92/14.25 9547x 9582 9583 9584 9585 9586 9587x 9588x 9589 9590x % 13.92/14.25 9591x 9592x 9593x 9594 9595 9596x 9597x 9598 9599 9600 % 13.92/14.25 9601 9602 9603 9604 9605x 9606x 9607 9608x 9609x 9610x % 13.92/14.25 9611x 9612 9613 9614x 9615x 9616 9617 9618 9619 9620 % 13.92/14.25 9621 9622 9623x 9624x 9625 9626x 9627x 9628x 9629x 9630 % 13.92/14.25 9631 9632x 9633x 9634 9635 9659 9660 9661 9662 9663 % 13.92/14.25 9664x 9665x 9666 9667x 9668x 9669x 9670x 9671 9672 9673x % 13.92/14.25 9674x 9675 9676 9677 9678 9679 9680 9681 9682x 9683x % 13.92/14.25 9684 9685x 9686x 9687x 9688x 9689 9690 9691x 9692x 9693 % 13.92/14.25 9694 9695 9696 9697 9698 9699 9700 9701 9702 9703 % 13.92/14.25 9704x 9705x 9706 9707x 9708x 9709x 9710 9711x 9712 9713 % 13.92/14.25 9714x 9715x 9716 9717 9718 9719 9720 9721 9722 9723 % 13.92/14.25 9724 9725 9726 9727 9728 9729x 9730x 9731 9732x 9733x % 13.92/14.25 9734x 9735 9736x 9737 9738 9739x 9740x 9741 9742 9743 % 13.92/14.25 9744 9767 9768 9769 9770 9771 9772 9773 9774 9775 % 13.92/14.25 9776 9777x 9778x 9779x 9780x 9781x 9782 9783x 9784 9785 % 13.92/14.25 9786x 9787x 9788 9789 9790 9791 9792 9793 9794 9795 % 13.92/14.25 9796 9797 9798 9799 9800 9801 9802x 9803x 9804x 9805x % 13.92/14.25 9806x 9807 9808x 9809 9810 9811x 9812x 9813 9814 9815 % 13.92/14.25 9816 9817 9818 9819 9820 9821 9822 9823 9824 9825 % 13.92/14.25 9826 9827x 9828x 9829x 9830x 9831x 9832 9833x 9834 9835 % 13.92/14.25 9836x 9837x 9838 9839 9840 9841 9863 9864 9865 9866 % 13.92/14.25 9867 9868 9869 9870 9871 9872 9873x 9874x 9875x 9876x % 13.92/14.25 9877x 9878 9879x 9880 9881 9882x 9883x 9884 9885 9886 % 13.92/14.25 9887 9888 9889 9890 9891 9892 9893 9894 9895 9896 % 13.92/14.25 9897 9898x 9899x 9900x 9901x 9902x 9903 9904x 9905 9906 % 13.92/14.25 9907x 9908x 9909 9910 9911 9912 9913 9914 9915 9916 % 13.92/14.25 9917 9918 9919 9920 9921 9922 9923x 9924x 9925x 9926x % 13.92/14.25 9927x 9928 9929x 9930 9931 9932x 9933x 9934 9935 9936 % 13.92/14.25 9937 9938 9939 9940 9941 9942 9943x 9944x 9945 9946x % 13.92/14.25 9947x 9948x 9949x 9950 9951 9952x 9953x 9954 9981 9982 % 13.92/14.25 9983 9984 9985 9986 9987 9988 9989 9990 9991 9992x % 13.92/14.25 9993x 9994x 9995x 9996x 9997x 9998 9999 10000x 10001x 10002 % 13.92/14.25 10003 10004 10005 10006 10007 10008 10009 10010 10011 10012 % 13.92/14.25 10013 10014 10015 10016x 10017x 10018x 10019x 10020x 10021x 10022 % 13.92/14.25 10023 10024x 10025x 10026 10027 10028 10032 10033 10052 10053 % 13.92/14.25 10054 10055 10056 10057 10058 10059 10060 10061 10062 10063 % 13.92/14.25 10064 10065 10066x 10067 10068 10069x 10070x 10071x 10072x 10073x % 13.92/14.25 10074 10075 10076x 10077x 10078 10079 10080 10081 10082 10083 % 13.92/14.25 10084 10085 10086 10087 10088 10089 10090 10091 10092 10093 % 13.92/14.25 10094 10095x 10096 10097 10098x 10099x 10100x 10101x 10102x 10103 % 13.92/14.25 10104 10105x 10106x 10107 10108 10109 10110 10111 10112 10113 % 13.92/14.25 10114 10115 10116 10117 10118 10119 10120 10121 10122x 10123x % 13.92/14.25 10124x 10125x 10126x 10127x 10128 10129 10130x 10131x 10132 10133 % 13.92/14.25 10134 10153 10154 10155 10156 10157 10158 10159 10160 10161 % 13.92/14.25 10162 10163 10164x 10165x 10166x 10167x 10168x 10169x 10170 10171 % 13.92/14.25 10172x 10173x 10174 10175 10176 10177 10178 10179 10180 10181 % 13.92/14.25 10182 10183 10184 10185 10186x 10187x 10188 10189x 10190x 10191x % 13.92/14.25 10192x 10193 10194 10195x 10196x 10197 10198 10210 10211 10212 % 13.92/14.25 10213 10214x 10215 10216 10217 10218 10219x 10220 10221x 10222x % 13.92/14.25 10223x 10224x 10225x 10226 10227 10228x 10229x 10230 10231 10232 % 13.92/14.25 10233 10234 10235 10236 10237 10250 10251 10252 10253 10254x % 13.92/14.25 10255 10256 10257 10258 10259 10260 10261 10262x 10263x 10264x % 13.92/14.25 10265x 10266x 10267 10268 10269x 10270x 10271 10272 10273 10274 % 13.92/14.25 10275 10276 10277 10278x 10279 10280 10281 10282 10283 10284 % 13.92/14.25 10285 10286x 10287x 10288x 10289x 10290x 10291 10292 10293x 10294x % 13.92/14.25 10295 10296 10297 10298 10299 10300 10301 10302x 10303 10304 % 13.92/14.25 10305 10306 10307 10308 10309 10310x 10311x 10312x 10313x 10314x % 13.92/14.25 10315 10316 10317x 10318x 10319 10320 10321 10322 10323 10324 % 13.92/14.25 10325 10326x 10327 10328 10329 10330 10331 10332 10333 10334x % 13.92/14.25 10335x 10336x 10337x 10338x 10339 10340 10341x 10342x 10343 10344 % 13.92/14.25 10345 10417 10418 10419 10420 10421 10422x 10423 10424 10425 % 13.92/14.25 10426 10427 10428 10429 10430x 10431 10432 10433x 10434x 10435x % 13.92/14.25 10436x 10437 10438 10439x 10440x 10441 10442 10443 10444 10448 % 13.92/14.25 10449 10450 10451x 10452 10453 10454x 10455x 10456 10457x 10458x % 13.92/14.25 10459x 10460 10461 10462x 10463x 10464 10465 10495 10496 10497 % 13.92/14.25 10498 10499 10500 10501 10502 10503 10504 10505 10506x 10507x % 13.92/14.25 10508 10509x 10510 10511 10512 10513 10514 10515 10516 10517x % 13.92/14.25 10518 10519 10520 10521 10522 10523 10524 10525 10526 10527 % 13.92/14.25 10528 10529 10530 10531 10532 10533 10534 10535 10536 10537 % 13.92/14.25 10538 10539 10540 10541 10542 10543 10544 10545 10546 10547 % 13.92/14.25 10548 10549 10550x 10551x 10554 10555 10556 10557 10558x 10598 % 13.92/14.25 10599 10600 10601 10602 10603 10604 10605 10606 10607 10608 % 13.92/14.25 10609 10610 10611 10612 10613x 10614x 10615x 10616 10617x 10618x % 13.92/14.25 10619 10620x 10621x 10622x 10623 10624x 10625 10626x 10627 10628x % 13.92/14.25 10629 10630x 10631 10632 10633x 10634x 10635 10636x 10637 10638x % 13.92/14.25 10639 10640x 10641 10642x 10643 10644 10645 10646x 10647x 10648 % 13.92/14.25 10649x 10650 10651x 10652 10653x 10654x 10655x 10656 10657 10658 % 13.92/14.25 10659 10660 10661x 10662 10663x 10664 10665 10666x 10667 10668x % 13.92/14.25 10669x 10670x 10671x 10672x 10673x 10730x 10731x 10732 10733 10734 % 13.92/14.25 10735 10736 10737 10738 10739 10740x 10741 10742 10743 10744 % 13.92/14.25 10745x 10746x 10747x 10748x 10749x 10750 10751 10752x 10753x 10754 % 13.92/14.25 10755 10756 10757 10758x 10759x 10760 10761 10762 10763 10764 % 13.92/14.25 10765 10766 10767 10768x 10769 10770 10771 10772 10773x 10774x % 13.92/14.25 10775x 10776x 10777x 10778 10779 10780x 10781x 10782 10783 10784 % 13.92/14.25 10785 10808 10809 10821 10822 10823 10824 10825 10826 10827 % 13.92/14.25 10828 10829x 10830x 10831 10832 10833 10834 10835 10836x 10837 % 13.92/14.25 10838x 10839x 10840x 10841x 10842x 10843 10844 10845x 10846x 10847 % 13.92/14.25 10848 10861 10862 10863 10864 10865 10866 10867 10868 10869 % 13.92/14.25 10870 10886x 10887x 10888 10889 10890 10891 10892 10893 10894 % 13.92/14.25 10895 10896x 10897 10898 10899 10900 10901x 10902x 10903x 10904x % 13.92/14.25 10905x 10906 10907 10908x 10909x 10910 10911 10912 10913 10914 % 13.92/14.25 10915 10924x 10925x 10926 10927 10928 10929 10930 10931 10932 % 13.92/14.25 10933 10934x 10935 10936 10937 10938 10939x 10940x 10941x 10942x % 13.92/14.25 10943x 10944 10945 10946x 10947x 10948 10949 10950 10951 10952 % 13.92/14.25 10953 10954x 10955x 10956 10957 10958 10959 10960 10961 10962 % 13.92/14.25 10963 10964x 10965 10966 10967 10968 10969x 10970x 10971x 10972x % 13.92/14.25 10973x 10974 10975 10976x 10977x 10978 10979 10980 10981 10982 % 13.92/14.25 10983 10994 10995 10996 10997x 10998x 10999 11000 11001 11002 % 13.92/14.25 11003 11004 11005 11006 11007x 11008 11009 11010 11011 11012x % 13.92/14.25 11013x 11014x 11015x 11016x 11017 11018 11019x 11020x 11021 11022 % 13.92/14.25 11023 11024 11025 11026 11027x 11028x 11029 11030 11031 11032 % 13.92/14.25 11033 11034 11035 11036 11037x 11038 11039 11040 11041 11042x % 13.92/14.25 11043x 11044x 11045x 11046x 11047 11048 11049x 11050x 11051 11052 % 13.92/14.25 11053 11062x 11063 11064 11065 11066x 11067x 11068 11069 11070 % 13.92/14.25 11071 11072 11073 11074 11075 11076x 11077 11078 11079 11080 % 13.92/14.25 11081x 11082x 11083x 11084x 11085x 11086 11087 11088x 11089x 11090 % 13.92/14.25 11091 11092 11093 11094 11095 11096 11097 11098 11102x 11103x % 13.92/14.25 11104x 11111x 11112x 11113 11114 11115 11116 11117x 11118x 11119 % 13.92/14.25 11120 11121 11122 11123 11124 11125 11126 11127x 11128 11129 % 13.92/14.25 11130 11131 11132 11133x 11134 11135 11136x 11137x 11138x 11139x % 13.92/14.25 11140 11141 11142x 11143x 11144 11145 11146 11147x 11148x 11149 % 13.92/14.25 11150 11151 11152 11153 11154 11155 11156 11157x 11158 11159 % 13.92/14.25 11160 11161 11162 11163x 11164 11165 11166x 11167x 11168x 11169x % 13.92/14.25 11170 11171 11172x 11173x 11174 11175 11176 11177 11178 11179 % 13.92/14.25 11193 11194x 11195x 11196 11197 11198 11199 11200 11201 11202 % 13.92/14.25 11203 11204x 11205 11206 11207 11208 11209 11210x 11211 11212 % 13.92/14.25 11213x 11214x 11215x 11216x 11217 11218 11219x 11220x 11221 11222 % 13.92/14.25 11223 11224x 11225x 11226 11227 11228 11229 11230 11231 11232 % 13.92/14.25 11233 11234x 11235 11236 11237 11238 11239 11240x 11241 11242 % 13.92/14.25 11243x 11244x 11245x 11246x 11247x 11248x 11249x 11250x 11251 11252 % 13.92/14.25 11253 11254 11255 11256 11257 11258 11259 11270x 11271x 11272x % 13.92/14.25 11276x 11277x 11278x 11279x 11280x 11281 11282 11283 11284 11285 % 13.92/14.25 11286 11287 11288 11289x 11290 11291 11292 11293 11294x 11295x % 13.92/14.25 11296x 11297x 11298x 11299 11300 11301x 11302x 11303 11304 11305 % 13.92/14.25 11306 11307 11308 11309 11310 11311 11312 11313 11314 11325x % 13.92/14.25 11326x 11327 11328 11329 11330x 11331x 11332 11333 11334 11335 % 13.92/14.25 11336 11337 11338 11339 11340x 11341 11342 11343 11344 11345x % 13.92/14.25 11346x 11347x 11348x 11349x 11350 11351 11352x 11353x 11354 11355 % 13.92/14.25 11356 11357 11358 11359 11360 11361 11367x 11368x 11369x 11409x % 13.92/14.25 11410x 11411 11412 11413 11414 11415 11416 11417 11418 11419x % 13.92/14.25 11420 11421 11422 11423 11424x 11425x 11426x 11427x 11428x 11429 % 13.92/14.25 11430 11431x 11432x 11433 11434 11435 11436 11437 11438 11439 % 13.92/14.25 11440 11441 11442 11443 11518 11519 11520 11521 11522 11523 % 13.92/14.25 11524 11525 11526 11527 11528 11529 11530 11531 11532 11533 % 13.92/14.25 11545x 11546x 11547x 11548 11549 11550 11551 11552 11553 11554 % 13.92/14.25 11555 11556 11557 11558x 11559x 11560 11561 11562 11563 11564x % 13.92/14.25 11565 11566x 11567 11568 11569x 11570 11571 11572x 11573 11574 % 13.92/14.25 11575x 11576x 11577x 11578x 11579 11580 11581x 11582x 11583 11584 % 13.92/14.25 11585 11600 11601x 11602 11603 11604 11605 11606 11607 11608 % 13.92/14.25 11609 11610 11611 11612 11613 11614 11615 11616 11617 11618 % 13.92/14.25 11619 11620 11621 11622 11623x 11624 11625 11626 11627 11628 % 13.92/14.25 11629 11630 11631 11632 11633x 11634 11635 11636 11637 11638 % 13.92/14.25 11639 11640 11641 11642 11643 11644 11645 11646 11647 11648 % 13.92/14.25 11649 11650 11651 11652 11653 11654 11655 11656 11657 11658 % 13.92/14.25 11659 11660 11661 11662 11663 11664 11665x 11666x 11692x 11693x % 13.92/14.25 11694x 11695 11696 11697 11698 11699 11700x 11701 11702 11703x % 13.92/14.25 11704x 11705 11706 11707 11708 11709x 11710 11711 11712x 11713 % 13.92/14.25 11714 11715x 11716 11717x 11718 11719x 11720x 11721x 11722x 11723 % 13.92/14.25 11724 11725x 11726x 11727 11728 11729 11730 11731 11732 11733 % 13.92/14.25 11734 11755 11756x 11757x 11758 11759 11760x 11761 11762x 11763x % 13.92/14.25 11764 11765x 11766x 11767 11768x 11769x 11770x 11771 11772x 11773 % 13.92/14.25 11774x 11775 11776x 11777 11778x 11779 11780x 11781 11782 11783 % 13.92/14.25 11784x 11785x 11786x 11787x 11788x 11789x 11790x 11791x 11792x 11793x % 13.92/14.25 11794x 11795x 11796x 11797x 11798x 11799x 11800x 11801x 11802x 11803x % 13.92/14.25 11804x 11805x 11806x 11807x 11808x 11809x 11810x 11811x 11812x 11813x % 13.92/14.25 11814x 11815x 11816x 11817x 11818x 11819 11820x 11821x 11822x 11823x % 13.92/14.25 11824x 11825x 11826x 11827x 11828x 11829x 11830x 11831x 11832x 11833x % 13.92/14.25 11834 11835 11836x 11837 11838x 11839 11840 11841x 11842 11843x % 13.92/14.25 11844x 11845x 11846x 11847x 11848x 11861 11862 11863 11864 11865 % 13.92/14.25 11866 11867 11868 11869 11870 11871 11872 11891x 11892x 11910x % 13.92/14.25 11911x 11912x 11913 11914 11915x 11916 11917x 11918x 11919 11920 % 13.92/14.25 11921 11922 11923 11924 11925x 11926 11927x 11928 11929x 11930x % 13.92/14.25 11931x 11932x 11933x 11934x 11935x 11936x 11937x 11938x 11939 11940 % 13.92/14.25 11941 11942 11943 11944 11945 11946 11947 11948 11949x 11950x % 13.92/14.25 11951 11952x 11953x 11954 11955 11956 11957 11958x 11959 11960x % 13.92/14.25 11961x 11962x 11963x 11964 11965x 11966x 11967x 11968x 11969x 11970x % 13.92/14.25 11971x 11972x 11973x 11974x 11975 11976 11977 11978 11979 11987x % 13.92/14.25 11988x 11999x 12000x 12001x 12002 12003 12004 12005 12006 12007 % 13.92/14.25 12008 12009 12010 12011 12012 12013 12034x 12035x 12036x 12037 % 13.92/14.25 12038 12039 12040 12041 12042 12043 12044 12045x 12046x 12047 % 13.92/14.25 12048x 12049x 12050 12051 12052 12053 12054x 12055 12056x 12057 % 13.92/14.25 12058 12059x 12060x 12061 12062x 12063x 12064x 12065x 12066 12067 % 13.92/14.25 12068x 12069x 12070 12071 12072 12073 12074 12075 12076 12077 % 13.92/14.25 12091x 12092x 12095 12096 12097x 12098x 12099x 12100x 12101x 12106x % 13.92/14.25 12107x 12108 12109 12110 12111 12112 12113 12114 12115 12116 % 13.92/14.25 12117 12118 12119 12122x 12123x 12124x 12125x 12126x 12129x 12130x % 13.92/14.25 12131x 12132x 12137x 12138x 12139x 12140 12141 12142 12143 12144 % 13.92/14.25 12145x 12146 12147 12148x 12149x 12150 12151 12152 12153 12154 % 13.92/14.25 12155 12156x 12157 12158x 12159x 12160x 12161x 12162x 12163x 12164x % 13.92/14.25 12165x 12166x 12167x 12168 12169 12170 12171x 12172x 12173 12174 % 13.92/14.25 12175 12176x 12177x 12178 12179x 12180x 12181 12182 12183 12184 % 13.92/14.25 12185 12186 12187x 12188 12189 12190x 12191x 12192x 12193x 12194x % 13.92/14.25 12195 12196x 12197x 12198x 12199 12200 12201 12202 12203 12204 % 13.92/14.25 12205 12206 12207 12208 12209 12210x 12211 12212 12213 12214x % 13.92/14.25 12215x 12216 12217 12218 12219 12220 12221 12222x 12223 12224 % 13.92/14.25 12225x 12226 12227x 12228x 12229x 12230x 12231 12232 12233x 12234x % 13.92/14.25 12235 12236 12237 12248x 12249x 12250x 12251 12252 12253 12254 % 13.92/14.25 12255 12256x 12257 12258 12259 12260x 12261x 12262 12263 12264 % 13.92/14.25 12265 12266 12267 12268x 12269 12270 12271x 12272 12273x 12274x % 13.92/14.25 12275x 12276x 12277 12278 12279x 12280x 12281 12282 12283 12284 % 13.92/14.25 12285 12286 12287 12288 12289 12290 12291x 12292 12293x 12294x % 13.92/14.25 12295 12296 12297 12298 12299 12300 12301x 12302 12303 12304x % 13.92/14.25 12305x 12306x 12307x 12308x 12309x 12310x 12311x 12312x 12313 12314 % 13.92/14.25 12315 12316 12317 12318 12336 12337 12338 12339 12340x 12341 % 13.92/14.25 12342x 12343x 12344 12345 12346 12347 12348 12349 12350x 12351 % 13.92/14.25 12352 12353x 12354x 12355x 12356x 12357x 12358 12359 12360x 12361x % 13.92/14.25 12362 12363 12364 12365 12366 12367 12368 12369 12370 12371 % 13.92/14.25 12372x 12373 12374 12375x 12376x 12377 12378 12379 12380 12381 % 13.92/14.25 12382 12383 12384x 12385x 12386 12387x 12388x 12389x 12390x 12391x % 13.92/14.25 12392x 12393x 12394x 12395x 12396x 12397x 12398 12399 12400 12401 % 13.92/14.25 12402 12403 12404 12409 12413x 12414x 12415x 12421x 12422x 12423x % 13.92/14.25 12424 12425 12426 12427 12428x 12429 12430 12431x 12432x 12433 % 13.92/14.25 12434 12435 12436 12437 12438 12439 12440x 12441 12442 12443 % 13.92/14.25 12444x 12445 12446x 12447x 12448x 12449x 12450 12451 12452x 12453x % 13.92/14.25 12454 12455 12456 12457 12458 12459 12460 12461 12462x 12463 % 13.92/14.25 12464 12465x 12466x 12467 12468 12469 12470 12471 12472 12473 % 13.92/14.25 12474x 12475x 12476 12477x 12478x 12479x 12480x 12481x 12482x 12483x % 13.92/14.25 12484x 12485x 12486x 12487x 12488 12489 12490 12491 12492 12493x % 13.92/14.25 12494 12506x 12507x 12508 12531 12532x 12533 12534 12535x 12536x % 13.92/14.25 12537x 12538x 12539x 12540x 12541x 12542x 12543x 12544x 12545x 12546x % 13.92/14.25 12547x 12548x 12549x 12550x 12551x 12552x 12553x 12554x 12555x 12556x % 13.92/14.25 12557x 12558x 12559x 12560x 12561x 12562x 12563 12564 12565x 12585x % 13.92/14.25 12586x 12587x 12591x 12592x 12593x 12594x 12595x 12599x 12600x 12601x % 13.92/14.25 12602x 12603x 12604x 12605x 12606x 12607x 12608x 12609x 12610x 12611x % 13.92/14.25 12612x 12613x 12614x 12615x 12616x 12617x 12618x 12619x 12620x 12621x % 13.92/14.25 12622x 12623x 12624x 12625x 12626x 12627x 12628x 12629x 12630x 12631x % 22.42/22.70 12632x 12633x 12634x 12635x 12636x 12637x 12638x 12639x 12640x 12641x % 22.42/22.70 12642x 12643x 12644x 12645x 12646x 12647x 12648x 12649x 12650x 12651x % 22.42/22.70 12652x 12653x 12654x 12655x 12656x 12657x 12658x 12659x 12660x 12661x % 22.42/22.70 12662x 12663x 12664x 12665x 12666x 12667x 12668x 12669x 12670x 12671x % 22.42/22.70 12672x 12673x 12674x 12675 12676x 12677x 12678x 12679x 12680x 12681x % 22.42/22.70 12682x 12683x 12684x 12685x 12686x 12687x 12688x 12689x 12690 12691 % 22.42/22.70 12692x 12693x 12694x 12695x 12696 12697x 12698x 12699x 12700x 12701x % 22.42/22.70 12702x 12703x 12704x 12705x 12706 12707 12708x 12709x 12710x 12711x % 22.42/22.70 12712x 12713x 12714x 12715x 12716x 12717x 12718x 12719x 12720x 12721x % 22.42/22.70 12722x 12723x 12724x 12725x 12726x 12727x 12728x 12729x 12730x 12731x % 22.42/22.70 12732x 12733x 12734x 12735x 12736 12737 12738 12739 12755x 12756x % 22.42/22.70 12757x 12758x 12759x 12760x 12761x 12762x 12763x 12764x 12765x 12766x % 22.42/22.70 12767x 12768x 12769x 12770x 12771x 12772x 12773x 12774x 12775x 12776x % 22.42/22.70 12777x 12778x 12779x 12780x 12781x 12782x 12783x 12784x 12785x 12786x % 22.42/22.70 12787x 12788x 12789x 12790x 12791x 12792x 12793x 12794x 12795x 12796x % 22.42/22.70 12797x 12798x 12799x 12800x 12801x 12802x 12803x 12804x 12805x 12806x % 22.42/22.70 12807x 12808x 12809x 12810x 12811x 12812x 12813x 12814x 12815x 12816x % 22.42/22.70 12817x 12818x 12819x 12820x 12824x 12825x 12826x 12827x 12828x 12832x % 22.42/22.70 12833x 12834x 12835x 12836x 12837x 12838x 12839x 12840x 12841x 12842x % 22.42/22.70 12843x 12844x 12845x 12846x 12847x 12848x 12849x 12850x 12851x 12852x % 22.42/22.70 12853x 12854x 12855x 12856x 12857x 12858x 12859x 12860x 12861x 12862x % 22.42/22.70 12863x 12864x 12865x 12866x 12867x 12868x 12869x 12870x 12871x 12872x % 22.42/22.70 12873x 12874x 12875x 12876x 12877x 12878x 12879x 12880x 12881x 12882x % 22.42/22.70 12883x 12884x 12885x 12886x 12887x 12888x 12889x 12890x 12891x 12892x % 22.42/22.70 12893x 12894x 12895x 12896x 12897x 12901x 12902x 12903x 12904x 12905x % 22.42/22.70 12906x 12907x 12908x 12909x 12910x 12911x 12912x 12913x 12914x 12915x % 22.42/22.70 12916x 12917x 12918x 12919x 12920x 12921x 12922x 12923x 12924x 12925x % 22.42/22.70 12926x 12927x 12928x 12929x 12930x 12931x 12932x 12933x 12934x 12935x % 22.42/22.70 12936x 12937x 12938x 12939x 12940x 12941x 12942x 12943x 12944x 12945x % 22.42/22.70 12946x 12947x 12948x 12949x 12950x 12951x 12952x 12953x 12954x 12955x % 22.42/22.70 12956x 12957x 12958x 12959x 12960x 12961x 12962x 12963x 12964x 12965x % 22.42/22.70 12966 12967 12968x 12969x 12970x 12971x 12972x 12973x 12974x 12975x % 22.42/22.70 12976x 12977x 12978x 12979x 12980x 12981x 12982x 12983x 12984x 12985x % 22.42/22.70 12986x 12987x 12988x 12989x 12990x 12991x 12992x 12993x 12994x 12995x % 22.42/22.70 12996x 12997x 12998x 12999x 13014x 13015x 13016x 13017x 13018x 13019x % 22.42/22.70 13023x 13024x 13025x 13026x 13027x 13028x 13032x 13033x 13034x 13035x % 22.42/22.70 13036x 13037x 13041x 13042x 13043x 13044x 13045x 13046x 13047 13048 % 22.42/22.70 13049x 13050x 13051x 13052x 13053x 13054x 13055x 13056x 13057x 13058x % 22.42/22.70 13059x 13060x 13061x 13062x 13063x 13064x 13065x 13066x 13067x 13068x % 22.42/22.70 13069x 13070x 13071x 13072x 13073x 13074x 13075x 13076x 13077x 13078 % 22.42/22.70 13079 13080x 13096x 13097x 13098x 13099x 13100x 13101x 13102x 13106x % 22.42/22.70 13107x 13108x 13109x 13110x 13111x 13112x 13113x 13114x 13115x 13116x % 22.42/22.70 13117x 13118x 13119x 13120x 13121x 13122x 13123x 13124x 13125x 13126x % 22.42/22.70 13127x 13128x 13129x 13130x 13131x 13132x 13133x 13134x 13135x 13136x % 22.42/22.70 13137x 13138x 13139x 13140x 13141x 13142x 13143x 13144x 13145x 13146x % 22.42/22.70 13147x 13148x 13149x 13150x 13151x 13152x 13153x 13154x 13155x 13156x % 22.42/22.70 13157x 13158x 13159x 13160x 13161x 13162x 13163x 13164x 13165x 13166x % 22.42/22.70 13167x 13168x 13169x 13170x 13171x 13172x 13173x 13177x 13178x 13179x % 22.42/22.70 13180x 13181x 13182x 13183x 13187x 13188x 13189x 13190x 13191x 13192x % 22.42/22.70 13193x 13194x 13195x 13196x 13197x 13198x 13199x 13200x 13201x 13202x % 22.42/22.70 13203x 13204x 13205x 13206x 13207x 13208x 13209x 13210x 13211x 13212x % 22.42/22.70 13213x 13214x 13215x 13216x 13217x 13218x 13219x 13220x 13221x 13222x % 22.42/22.70 13223x 13224x 13225x 13226x 13227x 13228x 13229x 13230x 13231x 13232x % 22.42/22.70 13233x 13234x 13235x 13236x 13237x 13238x 13239x 13240x 13241x 13242x % 22.42/22.70 13243x 13244x 13245x 13246x 13247x 13248x 13249x 13250x 13251x 13252x % 22.42/22.70 13253x 13254x 13255 13256x 13257 13279 13280x 13281 13282x 13283x % 22.42/22.70 13284x 13285 13286 13287 13288 13289 13290 13291 13292 13293 % 22.42/22.70 13294 13295 13296 13297Terminated % 299.75/300.02 Prover9 interrupted %------------------------------------------------------------------------------