%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX219+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n025.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 10.11s 10.46s % Output : Refutation 10.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX219+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.13/0.32 % Computer : n025.cluster.edu % 0.13/0.32 % Model : x86_64 x86_64 % 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.32 % Memory : 8042.1875MB % 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.32 % CPULimit : 300 % 0.13/0.32 % WCLimit : 300 % 0.13/0.32 % DateTime : Wed Apr 29 01:54:43 EDT 2026 % 0.13/0.32 % CPUTime : % 0.41/1.02 ============================== Prover9 =============================== % 0.41/1.02 Prover9 (32) version 2009-11A, November 2009. % 0.41/1.02 Process 32242 was started by sandbox on n025.cluster.edu, % 0.41/1.02 Wed Apr 29 01:54:43 2026 % 0.41/1.02 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_32018_n025.cluster.edu". % 0.41/1.02 ============================== end of head =========================== % 0.41/1.02 % 0.41/1.02 ============================== INPUT ================================= % 0.41/1.02 % 0.41/1.02 % Reading from file /tmp/Prover9_32018_n025.cluster.edu % 0.41/1.02 % 0.41/1.02 set(prolog_style_variables). % 0.41/1.02 set(auto2). % 0.41/1.02 % set(auto2) -> set(auto). % 0.41/1.02 % set(auto) -> set(auto_inference). % 0.41/1.02 % set(auto) -> set(auto_setup). % 0.41/1.02 % set(auto_setup) -> set(predicate_elim). % 0.41/1.02 % set(auto_setup) -> assign(eq_defs, unfold). % 0.41/1.02 % set(auto) -> set(auto_limits). % 0.41/1.02 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.41/1.02 % set(auto_limits) -> assign(sos_limit, 20000). % 0.41/1.02 % set(auto) -> set(auto_denials). % 0.41/1.02 % set(auto) -> set(auto_process). % 0.41/1.02 % set(auto2) -> assign(new_constants, 1). % 0.41/1.02 % set(auto2) -> assign(fold_denial_max, 3). % 0.41/1.02 % set(auto2) -> assign(max_weight, "200.000"). % 0.41/1.02 % set(auto2) -> assign(max_hours, 1). % 0.41/1.02 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.41/1.02 % set(auto2) -> assign(max_seconds, 0). % 0.41/1.02 % set(auto2) -> assign(max_minutes, 5). % 0.41/1.02 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.41/1.02 % set(auto2) -> set(sort_initial_sos). % 0.41/1.02 % set(auto2) -> assign(sos_limit, -1). % 0.41/1.02 % set(auto2) -> assign(lrs_ticks, 3000). % 0.41/1.02 % set(auto2) -> assign(max_megs, 400). % 0.41/1.02 % set(auto2) -> assign(stats, some). % 0.41/1.02 % set(auto2) -> clear(echo_input). % 0.41/1.02 % set(auto2) -> set(quiet). % 0.41/1.02 % set(auto2) -> clear(print_initial_clauses). % 0.41/1.02 % set(auto2) -> clear(print_given). % 0.41/1.02 assign(lrs_ticks,-1). % 0.41/1.02 assign(sos_limit,10000). % 0.41/1.02 assign(order,kbo). % 0.41/1.02 set(lex_order_vars). % 0.41/1.02 clear(print_given). % 0.41/1.02 % 0.41/1.02 % formulas(sos). % not echoed (32 formulas) % 0.41/1.02 % 0.41/1.02 ============================== end of input ========================== % 0.41/1.02 % 0.41/1.02 % From the command line: assign(max_seconds, 300). % 0.41/1.02 % 0.41/1.02 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.41/1.02 % 0.41/1.02 % Formulas that are not ordinary clauses: % 0.41/1.02 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 2 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 4 (all X all X2 proj1Arr(arr(X,X2)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 5 (all X all X2 proj2Arr(arr(X,X2)) = X2) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 6 (all X all X2 arr(X,X2) != a) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 7 (all X all X2 arr(X,X2) != b) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 8 (all X all X2 arr(X,X2) != c) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 9 (all X proj1Suc(suc(X)) = X) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 10 (all X zero != suc(X)) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 11 (all X proj1Just(just(X)) = X) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 12 (all X nothing != just(X)) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 13 (all X all X2 all X3 proj1App(app(X,X2,X3)) = X) # label(axiom_016) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 14 (all X all X2 all X3 proj2App(app(X,X2,X3)) = X2) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 15 (all X all X2 all X3 proj3App(app(X,X2,X3)) = X3) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 16 (all X proj1Lam(lam(X)) = X) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 17 (all X proj1Var(var(X)) = X) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 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.41/1.02 19 (all X al % 0.41/1.02 WARNING: denials share constants (see output). % 0.41/1.02 % 0.73/1.72 l X2 all X3 all X4 app(X,X2,X3) != var(X4)) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.72 20 (all X all X2 lam(X) != var(X2)) # label(axiom_023) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.72 21 (all Y index(nil,Y) = nothing) # label(axiom_024) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.72 22 (all Z all Xs index(cons(Z,Xs),zero) = just(Z)) # label(axiom_025) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.72 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]. % 0.73/1.72 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]. % 0.73/1.72 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]. % 0.73/1.72 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]. % 0.73/1.72 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]. % 0.73/1.72 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]. % 0.73/1.72 29 -(exists E tc(nil,E,arr(arr(b,c),arr(arr(a,b),arr(a,c))))) # label(goal_032) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.73/1.72 % 0.73/1.72 ============================== end of process non-clausal formulas === % 0.73/1.72 % 0.73/1.72 ============================== PROCESS INITIAL CLAUSES =============== % 0.73/1.72 % 0.73/1.72 ============================== PREDICATE ELIMINATION ================= % 0.73/1.72 % 0.73/1.72 ============================== end predicate elimination ============= % 0.73/1.72 % 0.73/1.72 Auto_denials: % 0.73/1.72 % copying label axiom_009 to answer in negative clause % 0.73/1.72 % copying label axiom_010 to answer in negative clause % 0.73/1.72 % copying label axiom_011 to answer in negative clause % 0.73/1.72 % copying label axiom_013 to answer in negative clause % 0.73/1.72 % copying label axiom_015 to answer in negative clause % 0.73/1.72 % copying label axiom_003 to answer in negative clause % 0.73/1.72 % copying label axiom_006 to answer in negative clause % 0.73/1.72 % copying label axiom_007 to answer in negative clause % 0.73/1.72 % copying label axiom_008 to answer in negative clause % 0.73/1.72 % copying label axiom_023 to answer in negative clause % 0.73/1.72 % copying label axiom_021 to answer in negative clause % 0.73/1.72 % copying label axiom_022 to answer in negative clause % 0.73/1.72 % copying label axiom_030 to answer in negative clause % 0.73/1.72 % copying label goal_032 to answer in negative clause % 0.73/1.72 % assign(max_proofs, 14). % (Horn set with more than one neg. clause) % 0.73/1.72 % 0.73/1.72 WARNING, because some of the denials share constants, % 0.73/1.72 some of the denials or their descendents may be subsumed, % 0.73/1.72 preventing the target number of proofs from being found. % 0.73/1.72 The shared constants are: nil, nothing, c, b, a. % 0.73/1.72 % 0.73/1.72 Term ordering decisions: % 0.73/1.72 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. % 0.73/1.72 % 0.73/1.72 ============================== end of process initial clauses ======== % 0.73/1.72 % 0.73/1.72 ============================== CLAUSES FOR SEARCH ==================== % 0.73/1.72 % 0.73/1.72 ============================== end of clauses for search ============= % 0.73/1.72 % 0.73/1.72 ============================== SEARCH ================================ % 0.73/1.72 % 0.73/1.72 % Starting search at 0.01 seconds. % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=52.000, iters=3444 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=51.000, iters=3412 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=49.000, iters=3357 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=46.000, iters=3387 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=43.000, iters=3348 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=42.000, iters=3360 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=41.000, iters=3371 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=40.000, iters=3412 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=38.000, iters=3346 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=37.000, iters=3368 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=36.000, iters=3333 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=35.000, iters=3367 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=34.000, iters=3355 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=33.000, iters=3380 % 0.73/1.72 % 0.73/1.72 Low Water (keep): wt=32.000, iters=3420 % 10.11/10.46 % 10.11/10.46 Low Water (keep): wt=31.000, iters=3349 % 10.11/10.46 % 10.11/10.46 Low Water (keep): wt=30.000, iters=3336 % 10.11/10.46 % 10.11/10.46 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 311 (0.00 of 2.29 sec). % 10.11/10.46 % 10.11/10.46 Low Water (keep): wt=29.000, iters=3334 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=3214, wt=76.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=3226, wt=75.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=3527, wt=69.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=3205, wt=68.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=3217, wt=65.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=3231, wt=64.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=9327, wt=34.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=10213, wt=32.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=11076, wt=28.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=9331, wt=26.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=7701, wt=25.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=11040, wt=24.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=11278, wt=22.000 % 10.11/10.46 % 10.11/10.46 Low Water (displace): id=11279, wt=20.000 % 10.11/10.46 % 10.11/10.46 ============================== PROOF ================================= % 10.11/10.46 % SZS status Theorem % 10.11/10.46 % SZS output start Refutation % 10.11/10.46 % 10.11/10.46 % Proof 1 at 9.24 (+ 0.21) seconds: goal_032. % 10.11/10.46 % Length of proof is 25. % 10.11/10.46 % Level of proof is 6. % 10.11/10.46 % Maximum clause weight is 26.000. % 10.11/10.46 % Given clauses 1126. % 10.11/10.46 % 10.11/10.46 15 (all X all X2 all X3 proj3App(app(X,X2,X3)) = X3) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 10.11/10.46 22 (all Z all Xs index(cons(Z,Xs),zero) = just(Z)) # label(axiom_025) # label(axiom) # label(non_clause). [assumption]. % 10.11/10.46 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]. % 10.11/10.46 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]. % 10.11/10.46 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]. % 10.11/10.46 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]. % 10.11/10.46 29 -(exists E tc(nil,E,arr(arr(b,c),arr(arr(a,b),arr(a,c))))) # label(goal_032) # label(negated_conjecture) # label(non_clause). [assumption]. % 10.11/10.46 41 proj3App(app(A,B,C)) = C # label(axiom_018) # label(axiom). [clausify(15)]. % 10.11/10.46 42 index(cons(A,B),zero) = just(A) # label(axiom_025) # label(axiom). [clausify(22)]. % 10.11/10.46 43 index(cons(A,B),suc(C)) = index(B,C) # label(axiom_026) # label(axiom). [clausify(23)]. % 10.11/10.46 60 -tc(nil,A,arr(arr(b,c),arr(arr(a,b),arr(a,c)))) # label(goal_032) # label(negated_conjecture) # answer(goal_032). [clausify(29)]. % 10.11/10.46 65 tc(A,lam(B),arr(C,D)) | -tc(cons(C,A),B,D) # label(axiom_029) # label(axiom). [clausify(26)]. % 10.11/10.46 67 index(A,B) != just(C) | tc(A,var(B),D) | C != D # label(axiom_031) # label(axiom). [clausify(28)]. % 10.11/10.46 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)]. % 10.11/10.46 75 -tc(cons(arr(b,c),nil),A,arr(arr(a,b),arr(a,c))) # answer(goal_032). [ur(65,a,60,a)]. % 10.11/10.46 102 tc(cons(A,B),var(zero),A). [hyper(67,a,42,a,c,41,a),rewrite([41(2)])]. % 10.11/10.46 104 index(A,B) != just(C) | tc(cons(D,A),var(suc(B)),E) | C != E. [para(43(a,1),67(a,1))]. % 10.11/10.46 290 -tc(cons(arr(a,b),cons(arr(b,c),nil)),A,arr(a,c)) # answer(goal_032). [ur(65,a,75,a)]. % 10.11/10.46 305 tc(cons(A,cons(B,C)),var(suc(zero)),B). [hyper(104,a,42,a,c,41,a),rewrite([41(2)])]. % 10.11/10.46 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))]. % 10.11/10.46 329 tc(cons(A,cons(arr(A,B),C)),app(var(suc(zero)),var(zero),A),B). [hyper(68,b,305,a,c,102,a)]. % 10.11/10.46 5133 tc(cons(A,cons(B,cons(C,D))),var(suc(suc(zero))),C). [hyper(307,a,42,a,c,41,a),rewrite([41(2)])]. % 10.11/10.46 5275 tc(cons(A,cons(arr(A,B),cons(arr(B,C),D))),app(var(suc(suc(zero))),app(var(suc(zero)),var(zero),A),B),C). [hyper(68,b,5133,a,c,329,a)]. % 10.11/10.46 12053 -tc(cons(a,cons(arr(a,b),cons(arr(b,c),nil))),A,c) # answer(goal_032). [ur(65,a,290,a)]. % 10.11/10.46 12054 $F # answer(goal_032). [resolve(12053,a,5275,a)]. % 10.11/10.46 % 10.11/10.46 % SZS output end Refutation % 10.11/10.46 ============================== end of proof ========================== % 10.11/10.46 % 10.11/10.46 % Disable descendants (x means already disabled): % 10.11/10.46 60 70 74x 75 132 139 145 146 181 196x % 10.11/10.46 197x 283 284 285 286 287 288 289 290 291x % 10.11/10.46 292 355 384 385 386 387 525 526 903x 904x % 10.11/10.46 1094 2065x 2066x 2704 2705 2812x 2813x 2814 2815x 2816x % 10.11/10.46 2817x 2818x 2819x 2820x 2821 2822 4227x 4228x 4229x 4230x % 10.11/10.46 4231x 4232x 4233x 4234x 4235x 4236 4237x 4443x 4444x 4445 % 10.11/10.46 4446 5136x 5137x 5141 5142 5143 5144 5145 5146 5147 % 10.11/10.46 5148 5149 5150 5151 5152 5153 5154 5155 5156 5157 % 10.11/10.46 5158 5159 5160 5161 5162 5163 5164 5165 5166 5167 % 10.11/10.46 5168 5169 5170 5171 5172 5173 5174 5175 5176 5177 % 10.11/10.46 5560 5561 5562 5641x 5642x 5643 5644 5645 5646 5647 % 10.11/10.46 5648 5649 5650 5651 5652 5653 5654 5655 5656 5657 % 10.11/10.46 5658 5659 5660 5661 5662x 5663 5664 5665 5733 5734 % 10.11/10.46 5735 5736x 5737x 5738 5739 5740 5981 5982 5983 5984 % 10.11/10.46 5985 5986 5987 5988 5989 5990 5991 5992 5993 5994 % 10.11/10.46 5995 5996 5997 5998 5999 6000 6001 6002 6003 6004 % 10.11/10.46 6005 6006 6007 6008 6009 6010 6011 6012 6013 6014 % 10.11/10.46 6015 6016 6017 6018 6019 6020 6021 6022 6228 6229 % 10.11/10.46 6230 6231 6232 6233 6234 6235 6236 6237 6238 6239 % 10.11/10.46 6240 6241 6242 6243 6244 6245 6246 6247 6248 6249 % 10.11/10.46 6250 6251 6252 6253 6254 6255 6256 6257 6258 6259 % 10.11/10.46 6260 6261 6262x 6263 6264x 6265 6266 6267 6268 6269 % 10.11/10.46 6270 6271 6272 6273 6274 6389 6390 6391 6392 6393 % 10.11/10.46 6394 6395 6396 6397 6398 6399 6400 6401 6402 6403 % 10.11/10.46 6404 6405 6406 6407 6408 6409 6410 6436 6437 6438 % 10.11/10.46 6439 6440 6441 6442 6443 6444 6445 6446x 6447x 6448x % 10.11/10.46 6449x 6552 6553 6554 6555 6556 6557 6558 6559 6560 % 10.11/10.46 6561 6562 6563 6564 6750 6751 6752 6753 6754 6755 % 10.11/10.46 6756 6757 6758 6759 6760 6761x 6762x 6763x 6764x 7030 % 10.11/10.46 7031 7032 7033 7034 7035 7036 7037 7038 7039 7040 % 10.11/10.46 7041 7042 7043 7044 7045 7046 7047 7048 7049 7050 % 10.11/10.46 7051 7052 7053 7103 7104 7105 7106 7107 7108 7109 % 10.11/10.46 7110 7111 7112 7113 7114 7115 7116 7117 7118 7119 % 10.11/10.46 7120 7121 7122 7123 7124 7125 7126 7127 7128 7129 % 10.11/10.46 7130 7131 7132 7133 7134 7208 7209 7210 7211 7212 % 10.11/10.46 7213 7214 7215 7216 7217 7218 7219 7220 7221 7222 % 10.11/10.46 7223 7224 7225 7226 7227 7228 7229 7230 7231 7232 % 10.11/10.46 7233 7234 7235 7236 7237 7238 7239 7240 7241 7242 % 10.11/10.46 7243 7244 7245 7246 7247 7248 7249 7250 7251 7252 % 10.11/10.46 7253 7254 7255 7256 7257 7258 7259 7260 7261 7262 % 10.11/10.46 7263 7343 7345 7346 7347 7348 7349 7350 7351 7352 % 10.11/10.46 7353 7354 7355 7356 7357 7358 7359 7360 7361 7362 % 10.11/10.46 7363 7364 7365 7366 7367 7368 7369 7370 7371 7431 % 10.11/10.46 7432 7433 7434 7435 7436 7437 7438 7439 7440 7441 % 10.11/10.46 7442 7443 7444 7445 7446 7447 7448 7449 7450 7451 % 10.11/10.46 7452 7453 7454 7455 7456 7457 7521 7522 7523 7524 % 10.11/10.46 7525 7526 7527 7528 7529 7530 7531 7532 7533 7534 % 10.11/10.46 7535 7536 7537 7538 7539 7540 7541 7542 7543 7544 % 10.11/10.46 7545 7546 7547 7548 7549 7550 7551 7552 7553 7554 % 10.11/10.46 7555 7556 7557 7558 7559 7560 7561 7562 7563 7564 % 10.11/10.46 7565 7566 7603 7604 7605 7606 7607 7608 7609 7610 % 10.11/10.46 7611 7612 7613 7614 7615 7616 7617 7618 7619 7620 % 10.11/10.46 7621 7622 7623 7624 7625 7626 7627 7628x 7629 7630x % 10.11/10.46 7631 7632 7633 7634 7635 7636 7637 7638 7639 7640 % 10.11/10.46 7641 7642 7643 7644 7645 7646 7688x 7689x 7690x 7691x % 10.11/10.46 7692x 7693x 7694x 7695x 7696x 7697x 7698x 7699x 7700 7701x % 10.11/10.46 7702 7703 7704 7705x 7706 7707x 7708 7709 7710 7711 % 10.11/10.46 7712 7713 7714 7715 7716 7717 7718 7719 7720 7721 % 10.11/10.46 7722x 7723 7724x 7725 7726x 7727 7728 7729 7730 7731 % 10.11/10.46 7732 7733 7734 7735 7736 7737 7738 7739 7740 7741 % 10.11/10.46 7742 7743 7744 7745x 7746 7747 7748 7749 7750 7751 % 10.11/10.46 7752 7753 7754 7755 7756 7757 7758 7759 7760 7791x % 10.11/10.46 7792 7793x 7794 7795 7796 7797 7798 7799 7800 7801 % 10.11/10.46 7802 7803 7804 7805 7806 7807 7808 7809 7810 7811 % 10.11/10.46 7812 7813 7814 7815 7816 7817 7818 7819 7820 7821 % 10.11/10.46 7822 7823 7824 7825 7826 7827 7828 7829 7830 7831 % 10.11/10.46 7832 7833 7834 7835 7836 7837 7838 7839 7840 7841 % 10.11/10.46 7842 7843 7844 7845 7846 7847 7848 7849 7850 7851 % 10.11/10.46 7852 7886 7887 7888 7889x 7890 7891 7892x 7893 7894 % 10.11/10.46 7895 7896 7897 7898 7899 7900 7901 7902 7903 7904 % 10.11/10.46 7905 7906 7907 8051 8052 8053 8054 8055 8056 8057 % 10.11/10.46 8058 8059 8060 8061 8062 8063 8064 8065 8066 8067 % 10.11/10.46 8068 8069 8070 8071 8072 8073 8074 8075 8076 8077 % 10.11/10.46 8078 8079 8080 8081x 8082x 8083x 8084x 8085x 8154 8155 % 10.11/10.46 8156 8157 8158 8159 8160 8161 8162 8163 8164 8165 % 10.11/10.46 8166 8167 8168 8169 8170 8171 8172 8173 8174 8175 % 10.11/10.46 8176 8177 8178 8179 8180 8181 8182 8183 8184x 8185x % 10.11/10.46 8186x 8187x 8188x 8561 8678 8679 8680 8681 8682 8683 % 10.11/10.46 8684 8685 8686 8687 8688 8689 8690 8691 8692 8693 % 10.11/10.46 8694 8695 8696 8697 8698 8699 8700 8701x 8813 8814 % 10.11/10.46 8815 8816 8817 8818 8819 8841 8842 8843 8844 8845 % 10.11/10.46 8846 8847 8848 8849 8850 8851 8870 8871 8872 8873 % 10.11/10.46 8874 8875 8876 8877 8878 9002 9003 9004 9023 9024 % 10.11/10.46 9025 9026 9027 9028 9029 9030 9031 9032 9050 9051 % 10.11/10.46 9052 9053 9054 9055 9056 9057 9058 9059 9060 9061 % 10.11/10.46 9062 9063 9064 9065 9066 9067 9068 9069 9070 9071 % 10.11/10.46 9072 9073 9074 9075 9076 9077 9078 9079 9080x 9081x % 10.11/10.46 9082x 9083x 9084x 9085 9086 9087 9088 9089 9090 9091 % 10.11/10.46 9092 9093 9094 9095 9111 9112 9113 9114 9115 9116 % 10.11/10.46 9297 9298 9299 9300 9301 9302 9303 9304 9305 9306 % 10.11/10.46 9307 9308 9309 9310 9311 9312 9313 9314 9315 9316 % 10.11/10.46 9317 9318 9319 9320 9321 9322 9323 9324 9325 9326 % 10.11/10.46 9327x 9328x 9329x 9330x 9331x 9564 9565 9566 9567 9568 % 10.11/10.46 9569 9570 9571 9572 9573 9574 9575 9576 9577 9578 % 10.11/10.46 9579 9580x 9581 9582 9583 9584 9585x 9586 9587 9588x % 10.11/10.46 9589 9590 9591 9592 9593 9594 9595 9596 9597 9598 % 10.11/10.46 9607 9608 9609 9610 9611 9612 9613 9614 9615 9616 % 10.11/10.46 9617 9618 9619 9620 9621x 9622 9623 9624 9625x 9626 % 10.11/10.46 9627 9628x 9629 9630 9631 9632 9633 9634 9635 9636 % 10.11/10.46 9637 9638 9639 9640 9641 9642 9643 9644 9645 9646 % 10.11/10.46 9647 9648 9649 9650 9651 9652 9653x 9654 9655 9656 % 10.11/10.46 9657x 9658 9659 9660x 9661 9662 9663 9664 9665 9680 % 10.11/10.46 9681 9682 9683 9684 9685 9686 9687 9688 9689 9690 % 10.11/10.46 9691 9692 9693 9694 9695 9696 9697 9698 9699x 9700 % 10.11/10.46 9701 9702 9703x 9704 9705 9706x 9707 9708 9709 9710 % 10.11/10.46 9711 9712 9713 9729 9730 9731 9732 9733 9734 9735 % 10.11/10.46 9736 9737 9738 9739 9740 9741 9742x 9743 9744 9745 % 10.11/10.46 9746 9747x 9748 9749 9750x 9751 9752 9753 9772 9773 % 10.11/10.46 9774 9775 9776 9777 9778x 9779 9780 9781 9782 9783x % 10.11/10.46 9784 9785 9786x 9787 9788 9789 9790 9791 9792 9793 % 10.11/10.46 9794 9795 9796x 9797 9798 9799 9800 9801x 9802 9803 % 10.11/10.46 9804x 9805 9806 9807 9808 9809 9810 9811 9812 9813 % 10.11/10.46 9814x 9815 9816 9817 9818 9819x 9820 9821 9822x 9823 % 10.11/10.46 9824 9825 9826 9827 9828 9829 9830 9831 9832x 9833 % 10.11/10.46 9834 9835 9836 9837x 9838 9839 9840x 9841 9842 9843 % 10.11/10.46 9857 9858 9859 9860 9861 9862 9863x 9864 9865 9866 % 10.11/10.46 9867 9868x 9869 9870 9871x 9872 9873 9874 9875 9876 % 10.11/10.46 9877 9878 9879 9880 9881x 9882 9883 9884 9885 9886x % 10.11/10.46 9887 9888 9889x 9890 9891 9892 9893 9894 9895 9896 % 10.11/10.46 9897 9898 9899 9900 9901 9902 9903 9904 9905x 9906 % 10.11/10.46 9907 9908 9909x 9910 9911 9912x 9913 9914 9915 9916 % 10.11/10.46 9917 9918 9919 9920 9921 9922 9923 9924 9925 9926 % 10.11/10.46 9927 9928 9929 9930x 9931 9932 9933 9934x 9935 9936 % 10.11/10.46 9937x 9938 9939 9940 9941 9942 9951 9952 9953 9954 % 10.11/10.46 9955 9956 9957 9958 9959 9960 9961 9962 9963 9964x % 10.11/10.46 9965 9966 9967 9968x 9969 9970 9971x 9972 9973 9974 % 10.11/10.46 9975 9976 9977 9978 9979 9980 9981 9982 9983 9984 % 10.11/10.46 9985 9986 9987 9988 9989 9990x 9991 9992 9993 9994x % 10.11/10.46 9995 9996 9997x 9998 9999 10000 10001 10002 10003 10004 % 10.11/10.46 10005 10006 10007 10008 10009 10010x 10011 10012 10013x 10014x % 10.11/10.46 10015x 10016 10017 10018x 10019x 10020 10021 10022 10023 10024 % 10.11/10.46 10025 10026 10027x 10028 10029 10030 10031 10032 10033 10034x % 10.11/10.46 10035x 10036x 10037x 10038x 10039 10040 10041x 10042x 10043 10044 % 10.11/10.46 10045 10050 10051 10052 10053 10054 10055 10056x 10057x 10058 % 10.11/10.46 10059 10060 10061 10062 10063 10064 10065 10066 10067 10068 % 10.11/10.46 10069 10070 10071 10072 10073 10074x 10075x 10076 10077x 10078x % 10.11/10.46 10079 10080 10081 10082x 10085 10086 10087 10088 10089 10090 % 10.11/10.46 10091 10092 10093 10094 10095 10102 10103 10104 10105 10106 % 10.11/10.46 10107 10108x 10109 10110 10111 10112 10113 10114 10115x 10116x % 10.11/10.46 10117x 10118x 10119x 10120 10121 10122x 10123x 10124 10125 10126 % 10.11/10.46 10127 10128 10129 10130 10131 10132 10133 10134 10135x 10136 % 10.11/10.46 10137 10138x 10139 10140 10141 10142x 10143 10144x 10145x 10146x % 10.11/10.46 10147x 10148x 10149 10150 10151x 10152x 10153 10154 10155 10164 % 10.11/10.46 10165 10166 10167 10168 10169 10170 10171 10172 10173 10174 % 10.11/10.46 10175 10176x 10177 10178 10179x 10180x 10181 10182x 10183x 10184 % 10.11/10.46 10185x 10186x 10187 10188x 10189 10190x 10191x 10192 10193x 10194x % 10.11/10.46 10195 10196 10197x 10198 10199 10200x 10201x 10202 10203 10204x % 10.11/10.46 10205x 10206 10207x 10208x 10209 10210 10211 10212 10213x 10214x % 10.11/10.46 10215x 10216x 10217x 10218 10219 10220 10221 10222 10223x 10224 % 10.11/10.46 10225 10226 10227 10228 10229 10230 10231 10232x 10233 10234 % 10.11/10.46 10235 10236 10237x 10238x 10239x 10240x 10241x 10242 10243 10244x % 10.11/10.46 10245x 10246 10247 10248 10249x 10250 10251 10252 10253 10254 % 10.11/10.46 10255 10256 10257 10258x 10259 10260 10261 10262 10263x 10264x % 10.11/10.46 10265x 10266x 10267x 10268 10269 10270x 10271x 10272 10273 10274 % 10.11/10.46 10287 10288 10289 10290 10291 10292 10293 10294 10295 10296 % 20.11/20.40 10307 10308 10315x 10316x 10317 10318 10319 10320 10321 10322 % 20.11/20.40 10323 10324 10325x 10326 10327 10328 10329 10330 10331x 10332 % 20.11/20.40 10333 10334x 10335x 10336x 10337x 10338 10339 10340x 10341x 10342 % 20.11/20.40 10343 10344 10345 10357 10358 10359 10360 10361 10362 10363 % 20.11/20.40 10364 10365 10366x 10367x 10368 10369 10370 10371 10372 10373 % 20.11/20.40 10374 10375 10376x 10377 10378 10379 10380 10381x 10382x 10383x % 20.11/20.40 10384x 10385x 10386 10387 10388x 10389x 10390 10391 10392 10405 % 20.11/20.40 10406 10407 10408x 10409x 10410 10411 10412 10413 10414 10415 % 20.11/20.40 10416 10417 10418x 10419 10420 10421 10422 10423x 10424x 10425x % 20.11/20.40 10426x 10427x 10428 10429 10430x 10431x 10432 10433 10434 10435 % 20.11/20.40 10436 10437 10438x 10439x 10440 10441 10442 10443 10444 10445 % 20.11/20.40 10446 10447 10448x 10449 10450 10451 10452 10453x 10454x 10455x % 20.11/20.40 10456x 10457x 10458 10459 10460x 10461x 10462 10463 10464 10474 % 20.11/20.40 10475 10476 10477 10478 10479 10480 10481 10482 10483 10484 % 20.11/20.40 10485 10497x 10498x 10499 10500 10501 10502 10503 10504 10505 % 20.11/20.40 10506 10507x 10508 10509 10510 10511 10512x 10513x 10514x 10515x % 20.11/20.40 10516x 10517 10518 10519x 10520x 10521 10522 10523 10524 10525 % 20.11/20.40 10526 10527 10528 10529 10530 10531 10540 10541 10542x 10543x % 20.11/20.40 10544 10545 10546 10547 10548 10549x 10550 10551 10552 10553x % 20.11/20.40 10554 10555 10556 10557x 10558x 10559x 10560x 10561x 10562x 10563 % 20.11/20.40 10564 10565x 10566x 10567 10568 10569 10570 10571 10572 10573 % 20.11/20.40 10574 10575 10576 10577 10578x 10579x 10580 10581 10582 10583 % 20.11/20.40 10584 10585x 10586 10587 10588 10589x 10590 10591 10592 10593x % 20.11/20.40 10594x 10595x 10596x 10597x 10598x 10599 10600 10601x 10602x 10603 % 20.11/20.40 10604 10605 10606 10615 10616 10617 10618 10619 10620 10621 % 20.11/20.40 10622 10623 10624 10625x 10626x 10627 10628 10629 10630 10631 % 20.11/20.40 10632 10633 10634 10635x 10636 10637 10638 10639 10640 10641x % 20.11/20.40 10642 10643 10644x 10645x 10646x 10647x 10648 10649 10650x 10651x % 20.11/20.40 10652 10653 10654 10655 10666 10667 10668 10669 10670 10671 % 20.11/20.40 10672 10673 10674 10675 10676 10686 10687 10688 10689 10690 % 20.11/20.40 10691 10692 10693 10694 10695 10696 10697 10707 10708 10709 % 20.11/20.40 10710 10711 10712x 10713x 10714 10715 10716 10717 10718 10719x % 20.11/20.40 10720 10721 10722 10723x 10724 10725 10726 10727 10728x 10729 % 20.11/20.40 10730 10731x 10732 10733 10734x 10735x 10736x 10737x 10738 10739 % 20.11/20.40 10740x 10741x 10742 10743 10744 10745 10746 10747 10748 10749 % 20.11/20.40 10765 10766 10767 10768 10769 10770 10771 10772 10773 10774 % 20.11/20.40 10775 10776 10789x 10790x 10791 10792 10793 10794 10795x 10796 % 20.11/20.40 10797x 10798 10799 10800x 10801 10802x 10803 10804 10805x 10806x % 20.11/20.40 10807x 10808x 10809 10810 10811x 10812x 10813 10814 10815 10816 % 20.11/20.40 10817 10818 10819x 10820x 10821 10822 10823 10824 10825 10826 % 20.11/20.40 10827 10828 10829x 10830 10831 10832 10833 10834x 10835x 10836x % 20.11/20.40 10837x 10838x 10839 10840 10841x 10842x 10843 10844 10845 10846 % 20.11/20.40 10847 10848 10857x 10858x 10859 10860 10861 10862 10863 10864 % 20.11/20.40 10865 10866 10867x 10868 10869 10870 10871 10872 10873 10874x % 20.11/20.40 10875 10876 10877x 10878x 10879x 10880x 10881 10882 10883x 10884x % 20.11/20.40 10885 10886 10887 10888 10889 10890x 10891x 10892 10893 10894 % 20.11/20.40 10895 10896 10897 10898 10899 10900x 10901 10902 10903 10904 % 20.11/20.40 10905 10906 10907x 10908 10909 10910x 10911x 10912x 10913x 10914 % 20.11/20.40 10915 10916x 10917x 10918 10919 10920 10921 10922 10923 10924 % 20.11/20.40 10925 10926 10927 11017x 11018x 11019 11020 11021 11022 11023 % 20.11/20.40 11024 11025 11026 11027x 11028 11029 11030 11031 11032x 11033 % 20.11/20.40 11034x 11035x 11036x 11037x 11038 11039 11040x 11041x 11042 11043 % 20.11/20.40 11044 11045 11046 11047 11048 11083 11084 11085 11086 11087 % 20.11/20.40 11088 11089 11090 11091 11092 11093 11119 11120 11121 11122 % 20.11/20.40 11123x 11124 11125 11126x 11127x 11128 11129 11130 11131 11132 % 20.11/20.40 11133 11134 11135 11136 11137 11138 11139 11140 11141 11142 % 20.11/20.40 11143 11144 11145 11146 11147 11148 11149 11150 11151 11152 % 20.11/20.40 11153 11154x 11155x 11156 11157x 11158x 11159 11160 11161 11162x % 20.11/20.40 11213x 11232x 11233x 11234x 11235x 11236x 11237x 11238 11239x 11240x % 20.11/20.40 11241x 11242 11243 11244 11245x 11246x 11247 11248x 11249 11250x % 20.11/20.40 11251 11252 11253 11254 11255x 11256 11257x 11258 11259x 11260x % 20.11/20.40 11261 11262 11263x 11264x 11265 11266x 11267x 11268 11269x 11270x % 20.11/20.40 11271 11272x 11273 11274x 11275x 11276 11277x 11278x 11279x 11280 % 20.11/20.40 11281x 11282 1Terminated % 299.73/300.02 Prover9 interrupted %------------------------------------------------------------------------------