%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX227+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n011.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 : Tue May 5 07:05:28 PM UTC 2026 % Result : Unknown 14.54s 14.72s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SWX227+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.16/0.35 % Computer : n011.cluster.edu % 0.16/0.35 % Model : x86_64 x86_64 % 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.35 % Memory : 8042.1875MB % 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.35 % CPULimit : 300 % 0.16/0.35 % WCLimit : 300 % 0.16/0.35 % DateTime : Tue May 5 12:52:02 EDT 2026 % 0.16/0.35 % CPUTime : % 2.02/2.22 ----- Otter 3.3f, August 2004 ----- % 2.02/2.22 The process was started by sandbox2 on n011.cluster.edu, % 2.02/2.22 Tue May 5 12:52:02 2026 % 2.02/2.22 The command was "./otter". The process ID is 28604. % 2.02/2.22 % 2.02/2.22 set(prolog_style_variables). % 2.02/2.22 set(auto). % 2.02/2.22 dependent: set(auto1). % 2.02/2.22 dependent: set(process_input). % 2.02/2.22 dependent: clear(print_kept). % 2.02/2.22 dependent: clear(print_new_demod). % 2.02/2.22 dependent: clear(print_back_demod). % 2.02/2.22 dependent: clear(print_back_sub). % 2.02/2.22 dependent: set(control_memory). % 2.02/2.22 dependent: assign(max_mem, 12000). % 2.02/2.22 dependent: assign(pick_given_ratio, 4). % 2.02/2.22 dependent: assign(stats_level, 1). % 2.02/2.22 dependent: assign(max_seconds, 10800). % 2.02/2.22 clear(print_given). % 2.02/2.22 % 2.02/2.22 formula_list(usable). % 2.02/2.22 all A (A=A). % 2.02/2.22 all X X2 (proj1(x(X,X2))=X). % 2.02/2.22 all X X2 (proj2(x(X,X2))=X2). % 2.02/2.22 all X X2 (x(X,X2)!=theVar). % 2.02/2.22 all X X2 (x(X,X2)!=k). % 2.02/2.22 all X X2 (x(X,X2)!=i). % 2.02/2.22 all X X2 (x(X,X2)!=s). % 2.02/2.22 all X X2 (x(X,X2)!=b). % 2.02/2.22 all X X2 (x(X,X2)!=c). % 2.02/2.22 theVar!=k. % 2.02/2.22 theVar!=i. % 2.02/2.22 theVar!=s. % 2.02/2.22 theVar!=b. % 2.02/2.22 theVar!=c. % 2.02/2.22 k!=i. % 2.02/2.22 k!=s. % 2.02/2.22 k!=b. % 2.02/2.22 k!=c. % 2.02/2.22 i!=s. % 2.02/2.22 i!=b. % 2.02/2.22 i!=c. % 2.02/2.22 s!=b. % 2.02/2.22 s!=c. % 2.02/2.22 b!=c. % 2.02/2.22 all X (proj1Suc(suc(X))=X). % 2.02/2.22 all X (suc(X)!=z). % 2.02/2.22 all X (proj1Just(just(X))=X). % 2.02/2.22 all X (nothing!=just(X)). % 2.02/2.22 all Y Z (fail(Y,Z)=par(Y,Z,step(Y),step(Z))). % 2.02/2.22 all X Y (par(X,Y,nothing,nothing)=nothing). % 2.02/2.22 all X Y U_red (par(X,Y,nothing,just(U_red))=just(x(X,U_red))). % 2.02/2.22 all X Y T_red (par(X,Y,just(T_red),nothing)=just(x(T_red,Y))). % 2.02/2.22 all X Y T_red U_red2 (par(X,Y,just(T_red),just(U_red2))=just(x(T_red,U_red2))). % 2.02/2.22 all X (X!=x(proj1(X),proj2(X))->step(X)=nothing). % 2.02/2.22 all Y Z (Y!=x(proj1(Y),proj2(Y))-> (Y!=i->step(x(Y,Z))=fail(Y,Z))). % 2.02/2.22 all Z X2 G (X2!=x(proj1(X2),proj2(X2))-> (X2!=k->step(x(x(X2,G),Z))=fail(x(X2,G),Z))). % 2.02/2.22 all Z G X3 F (X3!=s-> (X3!=b-> (X3!=c->step(x(x(x(X3,F),G),Z))=fail(x(x(X3,F),G),Z)))). % 2.02/2.22 all Z G F (step(x(x(x(s,F),G),Z))=just(x(x(F,Z),x(G,Z)))). % 2.02/2.22 all Z G F (step(x(x(x(b,F),G),Z))=just(x(F,x(G,Z)))). % 2.02/2.22 all Z G F (step(x(x(x(c,F),G),Z))=just(x(x(F,Z),G))). % 2.02/2.22 all Z G (step(x(x(k,G),Z))=just(G)). % 2.02/2.22 all Z (step(x(i,Z))=just(Z)). % 2.02/2.22 all X (X!=x(proj1(X),proj2(X))-> (X!=theVar-> -cheating(X))). % 2.02/2.22 all A B (cheating(x(A,B))<->cheating(A)|cheating(B)). % 2.02/2.22 cheating(theVar). % 2.02/2.22 all Y N (step(Y)=nothing->astep(suc(N),Y)=nothing). % 2.02/2.22 all Y N U (step(Y)=just(U)->astep(suc(N),Y)=astep(N,U)). % 2.02/2.22 all Y (astep(z,Y)=just(Y)). % 2.02/2.22 -(exists Y (-(astep(suc(suc(suc(suc(z)))),x(Y,theVar))=just(x(theVar,x(Y,theVar)))->cheating(Y)))). % 2.02/2.22 end_of_list. % 2.02/2.22 % 2.02/2.22 -------> usable clausifies to: % 2.02/2.22 % 2.02/2.22 list(usable). % 2.02/2.22 0 [] A=A. % 2.02/2.22 0 [] proj1(x(X,X2))=X. % 2.02/2.22 0 [] proj2(x(X,X2))=X2. % 2.02/2.22 0 [] x(X,X2)!=theVar. % 2.02/2.22 0 [] x(X,X2)!=k. % 2.02/2.22 0 [] x(X,X2)!=i. % 2.02/2.22 0 [] x(X,X2)!=s. % 2.02/2.22 0 [] x(X,X2)!=b. % 2.02/2.22 0 [] x(X,X2)!=c. % 2.02/2.22 0 [] theVar!=k. % 2.02/2.22 0 [] theVar!=i. % 2.02/2.22 0 [] theVar!=s. % 2.02/2.22 0 [] theVar!=b. % 2.02/2.22 0 [] theVar!=c. % 2.02/2.22 0 [] k!=i. % 2.02/2.22 0 [] k!=s. % 2.02/2.22 0 [] k!=b. % 2.02/2.22 0 [] k!=c. % 2.02/2.22 0 [] i!=s. % 2.02/2.22 0 [] i!=b. % 2.02/2.22 0 [] i!=c. % 2.02/2.22 0 [] s!=b. % 2.02/2.22 0 [] s!=c. % 2.02/2.22 0 [] b!=c. % 2.02/2.22 0 [] proj1Suc(suc(X))=X. % 2.02/2.22 0 [] suc(X)!=z. % 2.02/2.22 0 [] proj1Just(just(X))=X. % 2.02/2.22 0 [] nothing!=just(X). % 2.02/2.22 0 [] fail(Y,Z)=par(Y,Z,step(Y),step(Z)). % 2.02/2.22 0 [] par(X,Y,nothing,nothing)=nothing. % 2.02/2.22 0 [] par(X,Y,nothing,just(U_red))=just(x(X,U_red)). % 2.02/2.22 0 [] par(X,Y,just(T_red),nothing)=just(x(T_red,Y)). % 2.02/2.22 0 [] par(X,Y,just(T_red),just(U_red2))=just(x(T_red,U_red2)). % 2.02/2.22 0 [] X=x(proj1(X),proj2(X))|step(X)=nothing. % 2.02/2.22 0 [] Y=x(proj1(Y),proj2(Y))|Y=i|step(x(Y,Z))=fail(Y,Z). % 2.02/2.22 0 [] X2=x(proj1(X2),proj2(X2))|X2=k|step(x(x(X2,G),Z))=fail(x(X2,G),Z). % 2.02/2.22 0 [] X3=s|X3=b|X3=c|step(x(x(x(X3,F),G),Z))=fail(x(x(X3,F),G),Z). % 2.02/2.22 0 [] step(x(x(x(s,F),G),Z))=just(x(x(F,Z),x(G,Z))). % 2.02/2.22 0 [] step(x(x(x(b,F),G),Z))=just(x(F,x(G,Z))). % 2.02/2.22 0 [] step(x(x(x(c,F),G),Z))=just(x(x(F,Z),G)). % 2.02/2.22 0 [] step(x(x(k,G),Z))=just(G). % 2.02/2.22 0 [] step(x(i,Z))=just(Z). % 2.02/2.22 0 [] X=x(proj1(X),proj2(X))|X=theVar| -cheating(X). % 2.02/2.22 0 [] -cheating(x(A,B))|cheating(A)|cheating(B). % 2.02/2.22 0 [] cheating(x(A,B))| -cheating(A). % 2.02/2.22 0 [] cheating(x(A,B))| -cheating(B). % 2.02/2.22 0 [] cheating(theVar). % 2.02/2.22 0 [] step(Y)!=nothing|astep(suc(N),Y)=nothing. % 2.02/2.22 0 [] step(Y)!=just(U)|astep(suc(N),Y)=astep(N,U). % 2.02/2.22 0 [] astep(z,Y)=just(Y). % 2.02/2.22 0 [] astep(suc(suc(suc(suc(z)))),x(Y,theVar))!=just(x(theVar,x(Y,theVar)))|cheating(Y). % 2.02/2.22 end_of_list. % 2.02/2.22 % 2.02/2.22 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=4. % 2.02/2.22 % 2.02/2.22 This ia a non-Horn set with equality. The strategy will be % 2.02/2.22 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.02/2.22 deletion, with positive clauses in sos and nonpositive % 2.02/2.22 clauses in usable. % 2.02/2.22 % 2.02/2.22 dependent: set(knuth_bendix). % 2.02/2.22 dependent: set(anl_eq). % 2.02/2.22 dependent: set(para_from). % 2.02/2.22 dependent: set(para_into). % 2.02/2.22 dependent: clear(para_from_right). % 2.02/2.22 dependent: clear(para_into_right). % 2.02/2.22 dependent: set(para_from_vars). % 2.02/2.22 dependent: set(eq_units_both_ways). % 2.02/2.22 dependent: set(dynamic_demod_all). % 2.02/2.22 dependent: set(dynamic_demod). % 2.02/2.22 dependent: set(order_eq). % 2.02/2.22 dependent: set(back_demod). % 2.02/2.22 dependent: set(lrpo). % 2.02/2.22 dependent: set(hyper_res). % 2.02/2.22 dependent: set(unit_deletion). % 2.02/2.22 dependent: set(factor). % 2.02/2.22 % 2.02/2.22 ------------> process usable: % 2.02/2.22 ** KEPT (pick-wt=5): 1 [] x(A,B)!=theVar. % 2.02/2.22 ** KEPT (pick-wt=5): 2 [] x(A,B)!=k. % 2.02/2.22 ** KEPT (pick-wt=5): 3 [] x(A,B)!=i. % 2.02/2.22 ** KEPT (pick-wt=5): 4 [] x(A,B)!=s. % 2.02/2.22 ** KEPT (pick-wt=5): 5 [] x(A,B)!=b. % 2.02/2.22 ** KEPT (pick-wt=5): 6 [] x(A,B)!=c. % 2.02/2.22 ** KEPT (pick-wt=3): 7 [] theVar!=k. % 2.02/2.22 ** KEPT (pick-wt=3): 8 [] theVar!=i. % 2.02/2.22 ** KEPT (pick-wt=3): 9 [] theVar!=s. % 2.02/2.22 ** KEPT (pick-wt=3): 10 [] theVar!=b. % 2.02/2.22 ** KEPT (pick-wt=3): 11 [] theVar!=c. % 2.02/2.22 ** KEPT (pick-wt=3): 12 [] k!=i. % 2.02/2.22 ** KEPT (pick-wt=3): 14 [copy,13,flip.1] s!=k. % 2.02/2.22 ** KEPT (pick-wt=3): 15 [] k!=b. % 2.02/2.22 ** KEPT (pick-wt=3): 16 [] k!=c. % 2.02/2.22 ** KEPT (pick-wt=3): 18 [copy,17,flip.1] s!=i. % 2.02/2.22 ** KEPT (pick-wt=3): 19 [] i!=b. % 2.02/2.22 ** KEPT (pick-wt=3): 20 [] i!=c. % 2.02/2.22 ** KEPT (pick-wt=3): 21 [] s!=b. % 2.02/2.22 ** KEPT (pick-wt=3): 22 [] s!=c. % 2.02/2.22 ** KEPT (pick-wt=3): 24 [copy,23,flip.1] c!=b. % 2.02/2.22 ** KEPT (pick-wt=4): 25 [] suc(A)!=z. % 2.02/2.22 ** KEPT (pick-wt=4): 27 [copy,26,flip.1] just(A)!=nothing. % 2.02/2.22 ** KEPT (pick-wt=12): 29 [copy,28,flip.1] x(proj1(A),proj2(A))=A|A=theVar| -cheating(A). % 2.02/2.22 ** KEPT (pick-wt=8): 30 [] -cheating(x(A,B))|cheating(A)|cheating(B). % 2.02/2.22 ** KEPT (pick-wt=6): 31 [] cheating(x(A,B))| -cheating(A). % 2.02/2.22 ** KEPT (pick-wt=6): 32 [] cheating(x(A,B))| -cheating(B). % 2.02/2.22 ** KEPT (pick-wt=10): 33 [] step(A)!=nothing|astep(suc(B),A)=nothing. % 2.02/2.22 ** KEPT (pick-wt=13): 34 [] step(A)!=just(B)|astep(suc(C),A)=astep(C,B). % 2.02/2.22 ** KEPT (pick-wt=18): 35 [] astep(suc(suc(suc(suc(z)))),x(A,theVar))!=just(x(theVar,x(A,theVar)))|cheating(A). % 2.02/2.22 % 2.02/2.22 ------------> process sos: % 2.02/2.22 ** KEPT (pick-wt=3): 37 [] A=A. % 2.02/2.22 ** KEPT (pick-wt=6): 38 [] proj1(x(A,B))=A. % 2.02/2.22 ---> New Demodulator: 39 [new_demod,38] proj1(x(A,B))=A. % 2.02/2.22 ** KEPT (pick-wt=6): 40 [] proj2(x(A,B))=B. % 2.02/2.22 ---> New Demodulator: 41 [new_demod,40] proj2(x(A,B))=B. % 2.02/2.22 ** KEPT (pick-wt=5): 42 [] proj1Suc(suc(A))=A. % 2.02/2.22 ---> New Demodulator: 43 [new_demod,42] proj1Suc(suc(A))=A. % 2.02/2.22 ** KEPT (pick-wt=5): 44 [] proj1Just(just(A))=A. % 2.02/2.22 ---> New Demodulator: 45 [new_demod,44] proj1Just(just(A))=A. % 2.02/2.22 ** KEPT (pick-wt=11): 46 [] fail(A,B)=par(A,B,step(A),step(B)). % 2.02/2.22 ** KEPT (pick-wt=7): 47 [] par(A,B,nothing,nothing)=nothing. % 2.02/2.22 ---> New Demodulator: 48 [new_demod,47] par(A,B,nothing,nothing)=nothing. % 2.02/2.22 ** KEPT (pick-wt=11): 49 [] par(A,B,nothing,just(C))=just(x(A,C)). % 2.02/2.22 ** KEPT (pick-wt=11): 50 [] par(A,B,just(C),nothing)=just(x(C,B)). % 2.02/2.22 ** KEPT (pick-wt=12): 51 [] par(A,B,just(C),just(D))=just(x(C,D)). % 2.02/2.22 ** KEPT (pick-wt=11): 53 [copy,52,flip.1] x(proj1(A),proj2(A))=A|step(A)=nothing. % 2.02/2.22 ** KEPT (pick-wt=18): 55 [copy,54,flip.1] x(proj1(A),proj2(A))=A|A=i|step(x(A,B))=fail(A,B). % 2.02/2.22 ** KEPT (pick-wt=22): 57 [copy,56,flip.1] x(proj1(A),proj2(A))=A|A=k|step(x(x(A,B),C))=fail(x(A,B),C). % 2.02/2.22 ** KEPT (pick-wt=25): 58 [] A=s|A=b|A=c|step(x(x(x(A,B),C),D))=fail(x(x(A,B),C),D). % 2.02/2.22 ** KEPT (pick-wt=17): 59 [] step(x(x(x(s,A),B),C))=just(x(x(A,C),x(B,C))). % 2.02/2.22 ---> New Demodulator: 60 [new_demod,59] step(x(x(x(s,A),B),C))=just(x(x(A,C),x(B,C))). % 2.02/2.22 ** KEPT (pick-wt=15): 61 [] step(x(x(x(b,A),B),C))=just(x(A,x(B,C))). % 2.02/2.22 ---> New Demodulator: 62 [new_demod,61] step(x(x(x(b,A),B),C))=just(x(A,x(B,C))). % 2.02/2.22 ** KEPT (pick-wt=15): 63 [] step(x(x(x(c,A),B),C))=just(x(x(A,C),B)). % 2.02/2.22 ---> New Demodulator: 64 [new_demod,63] step(x(x(x(c,A),B),C))=just(x(x(A,C),B)). % 2.02/2.22 ** KEPT (pick-wt=9): 65 [] step(x(x(k,A),B))=just(A). % 2.02/2.22 ---> New Demodulator: 66 [new_demod,65] step(x(x(k,A),B))=just(A). % 2.02/2.22 ** KEPT (pick-wt=7): 67 [] step(x(i,A))=just(A). % 2.02/2.22 ---> New Demodulator: 68 [new_demod,67] step(x(i,A))=just(A). % 2.02/2.22 ** KEPT (pick-wt=2): 69 [] cheating(theVar). % 2.02/2.22 ** KEPT (pick-wt=6): 71 [copy,70,flip.1] just(A)=astep(z,A). % 2.02/2.22 ---> New Demodulator: 72 [new_demod,71] just(A)=astep(z,A). % 14.54/14.72 Following clause subsumed by 37 during input processing: 0 [copy,37,flip.1] A=A. % 14.54/14.72 >>>> Starting back demodulation with 39. % 14.54/14.72 >>>> Starting back demodulation with 41. % 14.54/14.72 >>>> Starting back demodulation with 43. % 14.54/14.72 >>>> Starting back demodulation with 45. % 14.54/14.72 ** KEPT (pick-wt=11): 73 [copy,46,flip.1] par(A,B,step(A),step(B))=fail(A,B). % 14.54/14.72 >>>> Starting back demodulation with 48. % 14.54/14.72 ** KEPT (pick-wt=13): 74 [copy,49,flip.1,demod,72,72] astep(z,x(A,B))=par(A,C,nothing,astep(z,B)). % 14.54/14.72 ** KEPT (pick-wt=13): 75 [copy,50,flip.1,demod,72,72] astep(z,x(A,B))=par(C,B,astep(z,A),nothing). % 14.54/14.72 ** KEPT (pick-wt=15): 76 [copy,51,flip.1,demod,72,72,72] astep(z,x(A,B))=par(C,D,astep(z,A),astep(z,B)). % 14.54/14.72 >>>> Starting back demodulation with 60. % 14.54/14.72 >>>> Starting back demodulation with 62. % 14.54/14.72 >>>> Starting back demodulation with 64. % 14.54/14.72 >>>> Starting back demodulation with 66. % 14.54/14.72 >>>> Starting back demodulation with 68. % 14.54/14.72 >>>> Starting back demodulation with 72. % 14.54/14.72 >> back demodulating 67 with 72. % 14.54/14.72 >> back demodulating 65 with 72. % 14.54/14.72 >> back demodulating 63 with 72. % 14.54/14.72 >> back demodulating 61 with 72. % 14.54/14.72 >> back demodulating 59 with 72. % 14.54/14.72 >> back demodulating 51 with 72. % 14.54/14.72 >> back demodulating 50 with 72. % 14.54/14.72 >> back demodulating 49 with 72. % 14.54/14.72 >> back demodulating 44 with 72. % 14.54/14.72 >> back demodulating 35 with 72. % 14.54/14.72 >> back demodulating 34 with 72. % 14.54/14.72 >> back demodulating 27 with 72. % 14.54/14.72 Following clause subsumed by 46 during input processing: 0 [copy,73,flip.1] fail(A,B)=par(A,B,step(A),step(B)). % 14.54/14.72 Following clause subsumed by 89 during input processing: 0 [copy,74,flip.1] par(A,B,nothing,astep(z,C))=astep(z,x(A,C)). % 14.54/14.72 Following clause subsumed by 88 during input processing: 0 [copy,75,flip.1] par(A,B,astep(z,C),nothing)=astep(z,x(C,B)). % 14.54/14.72 Following clause subsumed by 87 during input processing: 0 [copy,76,flip.1] par(A,B,astep(z,C),astep(z,D))=astep(z,x(C,D)). % 14.54/14.72 >>>> Starting back demodulation with 78. % 14.54/14.72 >>>> Starting back demodulation with 80. % 14.54/14.72 >>>> Starting back demodulation with 82. % 14.54/14.72 >>>> Starting back demodulation with 84. % 14.54/14.72 >>>> Starting back demodulation with 86. % 14.54/14.72 Following clause subsumed by 76 during input processing: 0 [copy,87,flip.1] astep(z,x(A,B))=par(C,D,astep(z,A),astep(z,B)). % 14.54/14.72 Following clause subsumed by 75 during input processing: 0 [copy,88,flip.1] astep(z,x(A,B))=par(C,B,astep(z,A),nothing). % 14.54/14.72 Following clause subsumed by 74 during input processing: 0 [copy,89,flip.1] astep(z,x(A,B))=par(A,C,nothing,astep(z,B)). % 14.54/14.72 >>>> Starting back demodulation with 91. % 14.54/14.72 % 14.54/14.72 ======= end of input processing ======= % 14.54/14.72 % 14.54/14.72 =========== start of search =========== % 14.54/14.72 % 14.54/14.72 % 14.54/14.72 Resetting weight limit to 10. % 14.54/14.72 % 14.54/14.72 % 14.54/14.72 Resetting weight limit to 10. % 14.54/14.72 % 14.54/14.72 sos_size=399 % 14.54/14.72 % 14.54/14.72 % 14.54/14.72 Resetting weight limit to 7. % 14.54/14.72 % 14.54/14.72 % 14.54/14.72 Resetting weight limit to 7. % 14.54/14.72 % 14.54/14.72 sos_size=397 % 14.54/14.72 % 14.54/14.72 Search stopped because sos empty. % 14.54/14.72 % 14.54/14.72 % 14.54/14.72 Search stopped because sos empty. % 14.54/14.72 % 14.54/14.72 ============ end of search ============ % 14.54/14.72 % 14.54/14.72 -------------- statistics ------------- % 14.54/14.72 clauses given 524 % 14.54/14.72 clauses generated 851524 % 14.54/14.72 clauses kept 566 % 14.54/14.72 clauses forward subsumed 2390 % 14.54/14.72 clauses back subsumed 2 % 14.54/14.72 Kbytes malloced 6835 % 14.54/14.72 % 14.54/14.72 ----------- times (seconds) ----------- % 14.54/14.72 user CPU time 12.49 (0 hr, 0 min, 12 sec) % 14.54/14.72 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 14.54/14.72 wall-clock time 14 (0 hr, 0 min, 14 sec) % 14.54/14.72 % 14.54/14.72 Process 28604 finished Tue May 5 12:52:16 2026 % 14.54/14.72 Otter interrupted % 14.54/14.72 PROOF NOT FOUND %------------------------------------------------------------------------------