%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV100+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n017.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 Jul 27 13:19:53 EDT 2022 % Result : Unknown 17.60s 17.77s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV100+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.06/0.13 % Command : otter-tptp-script %s % 0.12/0.34 % Computer : n017.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Jul 27 05:00:48 EDT 2022 % 0.12/0.34 % CPUTime : % 2.46/2.65 ----- Otter 3.3f, August 2004 ----- % 2.46/2.65 The process was started by sandbox on n017.cluster.edu, % 2.46/2.65 Wed Jul 27 05:00:48 2022 % 2.46/2.65 The command was "./otter". The process ID is 28000. % 2.46/2.65 % 2.46/2.65 set(prolog_style_variables). % 2.46/2.65 set(auto). % 2.46/2.65 dependent: set(auto1). % 2.46/2.65 dependent: set(process_input). % 2.46/2.65 dependent: clear(print_kept). % 2.46/2.65 dependent: clear(print_new_demod). % 2.46/2.65 dependent: clear(print_back_demod). % 2.46/2.65 dependent: clear(print_back_sub). % 2.46/2.65 dependent: set(control_memory). % 2.46/2.65 dependent: assign(max_mem, 12000). % 2.46/2.65 dependent: assign(pick_given_ratio, 4). % 2.46/2.65 dependent: assign(stats_level, 1). % 2.46/2.65 dependent: assign(max_seconds, 10800). % 2.46/2.65 clear(print_given). % 2.46/2.65 % 2.46/2.65 formula_list(usable). % 2.46/2.65 all A (A=A). % 2.46/2.65 all X Y (gt(X,Y)|gt(Y,X)|X=Y). % 2.46/2.65 all X Y Z (gt(X,Y)>(Y,Z)->gt(X,Z)). % 2.46/2.65 all X (-gt(X,X)). % 2.46/2.65 all X le_q(X,X). % 2.46/2.65 all X Y Z (le_q(X,Y)&le_q(Y,Z)->le_q(X,Z)). % 2.46/2.65 all X Y (lt(X,Y)<->gt(Y,X)). % 2.46/2.65 all X Y (ge_q(X,Y)<->le_q(Y,X)). % 2.46/2.65 all X Y (gt(Y,X)->le_q(X,Y)). % 2.46/2.65 all X Y (le_q(X,Y)&X!=Y->gt(Y,X)). % 2.46/2.65 all X Y (le_q(X,pred(Y))<->gt(Y,X)). % 2.46/2.65 all X gt(succ(X),X). % 2.46/2.65 all X Y (le_q(X,Y)->le_q(X,succ(Y))). % 2.46/2.65 all X Y (le_q(X,Y)<->gt(succ(Y),X)). % 2.46/2.65 all X C (le_q(n0,X)->le_q(uniform_int_rnd(C,X),X)). % 2.46/2.65 all X C (le_q(n0,X)->le_q(n0,uniform_int_rnd(C,X))). % 2.46/2.65 all I L U Val (le_q(L,I)&le_q(I,U)->a_select2(tptp_const_array1(dim(L,U),Val),I)=Val). % 2.46/2.65 all I L1 U1 J L2 U2 Val (le_q(L1,I)&le_q(I,U1)&le_q(L2,J)&le_q(J,U2)->a_select3(tptp_const_array2(dim(L1,U1),dim(L2,U2),Val),I,J)=Val). % 2.46/2.65 all A N ((all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(A,I,J)=a_select3(A,J,I)))-> (all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(trans(A),I,J)=a_select3(trans(A),J,I)))). % 2.46/2.65 all A N ((all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(A,I,J)=a_select3(A,J,I)))-> (all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(inv(A),I,J)=a_select3(inv(A),J,I)))). % 2.46/2.65 all A N ((all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(A,I,J)=a_select3(A,J,I)))-> (all I J K VAL (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)&le_q(n0,K)&le_q(K,N)->a_select3(tptp_update3(A,K,K,VAL),I,J)=a_select3(tptp_update3(A,K,K,VAL),J,I)))). % 2.46/2.65 all A B N ((all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(A,I,J)=a_select3(A,J,I)))& (all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(B,I,J)=a_select3(B,J,I)))-> (all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(tptp_madd(A,B),I,J)=a_select3(tptp_madd(A,B),J,I)))). % 2.46/2.65 all A B N ((all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(A,I,J)=a_select3(A,J,I)))& (all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(B,I,J)=a_select3(B,J,I)))-> (all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(tptp_msub(A,B),I,J)=a_select3(tptp_msub(A,B),J,I)))). % 2.46/2.65 all A B N ((all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(B,I,J)=a_select3(B,J,I)))-> (all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(tptp_mmul(A,tptp_mmul(B,trans(A))),I,J)=a_select3(tptp_mmul(A,tptp_mmul(B,trans(A))),J,I)))). % 2.46/2.65 all A B N M ((all I J (le_q(n0,I)&le_q(I,M)&le_q(n0,J)&le_q(J,M)->a_select3(B,I,J)=a_select3(B,J,I)))-> (all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(tptp_mmul(A,tptp_mmul(B,trans(A))),I,J)=a_select3(tptp_mmul(A,tptp_mmul(B,trans(A))),J,I)))). % 2.46/2.65 all A B C D E F N M ((all I J (le_q(n0,I)&le_q(I,M)&le_q(n0,J)&le_q(J,M)->a_select3(D,I,J)=a_select3(D,J,I)))& (all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(A,I,J)=a_select3(A,J,I)))& (all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(F,I,J)=a_select3(F,J,I)))-> (all I J (le_q(n0,I)&le_q(I,N)&le_q(n0,J)&le_q(J,N)->a_select3(tptp_madd(A,tptp_mmul(B,tptp_mmul(tptp_madd(tptp_mmul(C,tptp_mmul(D,trans(C))),tptp_mmul(E,tptp_mmul(F,trans(E)))),trans(B)))),I,J)=a_select3(tptp_madd(A,tptp_mmul(B,tptp_mmul(tptp_madd(tptp_mmul(C,tptp_mmul(D,trans(C))),tptp_mmul(E,tptp_mmul(F,trans(E)))),trans(B)))),J,I)))). % 2.46/2.65 all Body (sum(n0,tptp_minus_1,Body)=n0). % 2.46/2.65 all Body (tptp_float_0_0=sum(n0,tptp_minus_1,Body)). % 2.46/2.65 succ(tptp_minus_1)=n0. % 2.46/2.65 all X (plus(X,n1)=succ(X)). % 2.46/2.65 all X (plus(n1,X)=succ(X)). % 2.46/2.65 all X (plus(X,n2)=succ(succ(X))). % 2.46/2.65 all X (plus(n2,X)=succ(succ(X))). % 2.46/2.65 all X (plus(X,n3)=succ(succ(succ(X)))). % 17.60/17.77 all X (plus(n3,X)=succ(succ(succ(X)))). % 17.60/17.77 all X (plus(X,n4)=succ(succ(succ(succ(X))))). % 17.60/17.77 all X (plus(n4,X)=succ(succ(succ(succ(X))))). % 17.60/17.77 all X (plus(X,n5)=succ(succ(succ(succ(succ(X)))))). % 17.60/17.77 all X (plus(n5,X)=succ(succ(succ(succ(succ(X)))))). % 17.60/17.77 all X (minus(X,n1)=pred(X)). % 17.60/17.77 all X (pred(succ(X))=X). % 17.60/17.77 all X (succ(pred(X))=X). % 17.60/17.77 all X Y (le_q(succ(X),succ(Y))<->le_q(X,Y)). % 17.60/17.77 all X Y (le_q(succ(X),Y)->gt(Y,X)). % 17.60/17.77 all X Y (le_q(minus(X,Y),X)->le_q(n0,Y)). % 17.60/17.77 all X U V VAL (a_select3(tptp_update3(X,U,V,VAL),U,V)=VAL). % 17.60/17.77 all I J U V X VAL VAL2 (I!=U&J=V&a_select3(X,U,V)=VAL->a_select3(tptp_update3(X,I,J,VAL2),U,V)=VAL). % 17.60/17.77 all I J U V X VAL ((all I0 J0 (le_q(n0,I0)&le_q(n0,J0)&le_q(I0,U)&le_q(J0,V)->a_select3(X,I0,J0)=VAL))&le_q(n0,I)&le_q(I,U)&le_q(n0,J)&le_q(J,V)->a_select3(tptp_update3(X,U,V,VAL),I,J)=VAL). % 17.60/17.77 all X U VAL (a_select2(tptp_update2(X,U,VAL),U)=VAL). % 17.60/17.77 all I U X VAL VAL2 (I!=U&a_select2(X,U)=VAL->a_select2(tptp_update2(X,I,VAL2),U)=VAL). % 17.60/17.77 all I U X VAL ((all I0 (le_q(n0,I0)&le_q(I0,U)->a_select2(X,I0)=VAL))&le_q(n0,I)&le_q(I,U)->a_select2(tptp_update2(X,U,VAL),I)=VAL). % 17.60/17.77 true. % 17.60/17.77 def!=use. % 17.60/17.77 -(a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use&a_select2(rho_defuse,n2)=use&a_select2(sigma_defuse,n0)=use&a_select2(sigma_defuse,n1)=use&a_select2(sigma_defuse,n2)=use&a_select2(sigma_defuse,n3)=use&a_select2(sigma_defuse,n4)=use&a_select2(sigma_defuse,n5)=use&a_select3(u_defuse,n0,n0)=use&a_select3(u_defuse,n1,n0)=use&a_select3(u_defuse,n2,n0)=use&a_select2(xinit_defuse,n3)=use&a_select2(xinit_defuse,n4)=use&a_select2(xinit_defuse,n5)=use&a_select2(xinit_mean_defuse,n0)=use&a_select2(xinit_mean_defuse,n1)=use&a_select2(xinit_mean_defuse,n2)=use&a_select2(xinit_mean_defuse,n3)=use&a_select2(xinit_mean_defuse,n4)=use&a_select2(xinit_mean_defuse,n5)=use&a_select2(xinit_noise_defuse,n0)=use&a_select2(xinit_noise_defuse,n1)=use&a_select2(xinit_noise_defuse,n2)=use&a_select2(xinit_noise_defuse,n3)=use&a_select2(xinit_noise_defuse,n4)=use&a_select2(xinit_noise_defuse,n5)=use&le_q(n0,pv5)&le_q(pv5,minus(n999,n1))& (all A B (le_q(n0,A)&le_q(n0,B)&le_q(A,n2)&le_q(B,minus(pv5,n1))->a_select3(u_defuse,A,B)=use&a_select3(z_defuse,A,B)=use))-> (-gt(pv5,n0)-> (-gt(pv5,n0)->a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use&a_select2(rho_defuse,n2)=use&a_select2(sigma_defuse,n0)=use&a_select2(sigma_defuse,n1)=use&a_select2(sigma_defuse,n2)=use&a_select2(sigma_defuse,n3)=use&a_select2(sigma_defuse,n4)=use&a_select2(sigma_defuse,n5)=use&a_select3(u_defuse,n0,n0)=use&a_select3(u_defuse,n1,n0)=use&a_select3(u_defuse,n2,n0)=use&a_select2(xinit_defuse,n3)=use&a_select2(xinit_defuse,n4)=use&a_select2(xinit_defuse,n5)=use&a_select2(xinit_mean_defuse,n0)=use&a_select2(xinit_mean_defuse,n1)=use&a_select2(xinit_mean_defuse,n2)=use&a_select2(xinit_mean_defuse,n3)=use&a_select2(xinit_mean_defuse,n4)=use&a_select2(xinit_mean_defuse,n5)=use&a_select2(xinit_noise_defuse,n0)=use&a_select2(xinit_noise_defuse,n1)=use&a_select2(xinit_noise_defuse,n2)=use&a_select2(xinit_noise_defuse,n3)=use&a_select2(xinit_noise_defuse,n4)=use&a_select2(xinit_noise_defuse,n5)=use&le_q(n0,pv5)&le_q(pv5,minus(n999,n1))& (all C D (le_q(n0,C)&le_q(n0,D)&le_q(C,n2)&le_q(D,pv5)->a_select3(u_defuse,C,D)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(z_defuse,n0,pv5,use),n1,pv5,use),n2,pv5,use),C,D)=use))& (all E F (le_q(n0,E)&le_q(n0,F)&le_q(E,n2)&le_q(F,minus(pv5,n1))->a_select3(u_defuse,E,F)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(z_defuse,n0,pv5,use),n1,pv5,use),n2,pv5,use),E,F)=use)))& (gt(pv5,n0)->a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use&a_select2(rho_defuse,n2)=use&a_select2(sigma_defuse,n0)=use&a_select2(sigma_defuse,n1)=use&a_select2(sigma_defuse,n2)=use&a_select2(sigma_defuse,n3)=use&a_select2(sigma_defuse,n4)=use&a_select2(sigma_defuse,n5)=use&a_select3(u_defuse,n0,n0)=use&a_select3(u_defuse,n1,n0)=use&a_select3(u_defuse,n2,n0)=use&a_select2(xinit_defuse,n3)=use&a_select2(xinit_defuse,n4)=use&a_select2(xinit_defuse,n5)=use&a_select2(xinit_mean_defuse,n0)=use&a_select2(xinit_mean_defuse,n1)=use&a_select2(xinit_mean_defuse,n2)=use&a_select2(xinit_mean_defuse,n3)=use&a_select2(xinit_mean_defuse,n4)=use&a_select2(xinit_mean_defuse,n5)=use&a_select2(xinit_noise_defuse,n0)=use&a_select2(xinit_noise_defuse,n1)=use&a_select2(xinit_noise_defuse,n2)=use&a_select2(xinit_noise_defuse,n3)=use&a_select2(xinit_noise_defuse,n4)=use&a_select2(xinit_noise_defuse,n5)=use&le_q(n0,pv5)&le_q(pv5,minus(n999,n1))& (all G H (le_q(n0,G)&le_q(n0,H)&le_q(G,n2)&le_q(H,pv5)->a_select3(u_defuse,G,H)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(z_defuse,n0,pv5,use),n1,pv5,use),n2,pv5,use),G,H)=use))& (all I J (le_q(n0,I)&le_q(n0,J)&le_q(I,n2)&le_q(J,minus(pv5,n1))->a_select3(u_defuse,I,J)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(z_defuse,n0,pv5,use),n1,pv5,use),n2,pv5,use),I,J)=use))))& (gt(pv5,n0)-> (-gt(pv5,n0)->a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use&a_select2(rho_defuse,n2)=use&a_select2(sigma_defuse,n0)=use&a_select2(sigma_defuse,n1)=use&a_select2(sigma_defuse,n2)=use&a_select2(sigma_defuse,n3)=use&a_select2(sigma_defuse,n4)=use&a_select2(sigma_defuse,n5)=use&a_select2(xinit_defuse,n3)=use&a_select2(xinit_defuse,n4)=use&a_select2(xinit_defuse,n5)=use&a_select2(xinit_mean_defuse,n0)=use&a_select2(xinit_mean_defuse,n1)=use&a_select2(xinit_mean_defuse,n2)=use&a_select2(xinit_mean_defuse,n3)=use&a_select2(xinit_mean_defuse,n4)=use&a_select2(xinit_mean_defuse,n5)=use&a_select2(xinit_noise_defuse,n0)=use&a_select2(xinit_noise_defuse,n1)=use&a_select2(xinit_noise_defuse,n2)=use&a_select2(xinit_noise_defuse,n3)=use&a_select2(xinit_noise_defuse,n4)=use&a_select2(xinit_noise_defuse,n5)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n0,pv5,use),n1,pv5,use),n0,pv5,use),n2,pv5,use),n1,pv5,use),n2,pv5,use),n0,n0)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n0,pv5,use),n1,pv5,use),n0,pv5,use),n2,pv5,use),n1,pv5,use),n2,pv5,use),n1,n0)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n0,pv5,use),n1,pv5,use),n0,pv5,use),n2,pv5,use),n1,pv5,use),n2,pv5,use),n2,n0)=use&le_q(n0,pv5)&le_q(pv5,minus(n999,n1))& (all K L (le_q(n0,K)&le_q(n0,L)&le_q(K,n2)&le_q(L,pv5)->a_select3(tptp_update3(tptp_update3(tptp_update3(z_defuse,n0,pv5,use),n1,pv5,use),n2,pv5,use),K,L)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n0,pv5,use),n1,pv5,use),n0,pv5,use),n2,pv5,use),n1,pv5,use),n2,pv5,use),K,L)=use))& (all M N (le_q(n0,M)&le_q(n0,N)&le_q(M,n2)&le_q(N,minus(pv5,n1))->a_select3(tptp_update3(tptp_update3(tptp_update3(z_defuse,n0,pv5,use),n1,pv5,use),n2,pv5,use),M,N)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n0,pv5,use),n1,pv5,use),n0,pv5,use),n2,pv5,use),n1,pv5,use),n2,pv5,use),M,N)=use)))& (gt(pv5,n0)->a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use&a_select2(rho_defuse,n2)=use&a_select2(sigma_defuse,n0)=use&a_select2(sigma_defuse,n1)=use&a_select2(sigma_defuse,n2)=use&a_select2(sigma_defuse,n3)=use&a_select2(sigma_defuse,n4)=use&a_select2(sigma_defuse,n5)=use&a_select2(xinit_defuse,n3)=use&a_select2(xinit_defuse,n4)=use&a_select2(xinit_defuse,n5)=use&a_select2(xinit_mean_defuse,n0)=use&a_select2(xinit_mean_defuse,n1)=use&a_select2(xinit_mean_defuse,n2)=use&a_select2(xinit_mean_defuse,n3)=use&a_select2(xinit_mean_defuse,n4)=use&a_select2(xinit_mean_defuse,n5)=use&a_select2(xinit_noise_defuse,n0)=use&a_select2(xinit_noise_defuse,n1)=use&a_select2(xinit_noise_defuse,n2)=use&a_select2(xinit_noise_defuse,n3)=use&a_select2(xinit_noise_defuse,n4)=use&a_select2(xinit_noise_defuse,n5)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n0,pv5,use),n1,pv5,use),n0,pv5,use),n2,pv5,use),n1,pv5,use),n2,pv5,use),n0,n0)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n0,pv5,use),n1,pv5,use),n0,pv5,use),n2,pv5,use),n1,pv5,use),n2,pv5,use),n1,n0)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(tp % 17.60/17.77 Search stopped in tp_alloc by max_mem option. % 17.60/17.77 tp_update3(tptp_update3(tptp_update3(u_defuse,n0,pv5,use),n1,pv5,use),n0,pv5,use),n2,pv5,use),n1,pv5,use),n2,pv5,use),n2,n0)=use&le_q(n0,pv5)&le_q(pv5,minus(n999,n1))& (all O P (le_q(n0,O)&le_q(n0,P)&le_q(O,n2)&le_q(P,pv5)->a_select3(tptp_update3(tptp_update3(tptp_update3(z_defuse,n0,pv5,use),n1,pv5,use),n2,pv5,use),O,P)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n0,pv5,use),n1,pv5,use),n0,pv5,use),n2,pv5,use),n1,pv5,use),n2,pv5,use),O,P)=use))& (all Q R (le_q(n0,Q)&le_q(n0,R)&le_q(Q,n2)&le_q(R,minus(pv5,n1))->a_select3(tptp_update3(tptp_update3(tptp_update3(z_defuse,n0,pv5,use),n1,pv5,use),n2,pv5,use),Q,R)=use&a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n0,pv5,use),n1,pv5,use),n0,pv5,use),n2,pv5,use),n1,pv5,use),n2,pv5,use),Q,R)=use))))). % 17.60/17.77 gt(n5,n4). % 17.60/17.77 gt(n999,n4). % 17.60/17.77 gt(n999,n5). % 17.60/17.77 gt(n4,tptp_minus_1). % 17.60/17.77 gt(n5,tptp_minus_1). % 17.60/17.77 gt(n999,tptp_minus_1). % 17.60/17.77 gt(n0,tptp_minus_1). % 17.60/17.77 gt(n1,tptp_minus_1). % 17.60/17.77 gt(n2,tptp_minus_1). % 17.60/17.77 gt(n3,tptp_minus_1). % 17.60/17.77 gt(n4,n0). % 17.60/17.77 gt(n5,n0). % 17.60/17.77 gt(n999,n0). % 17.60/17.77 gt(n1,n0). % 17.60/17.77 gt(n2,n0). % 17.60/17.77 gt(n3,n0). % 17.60/17.77 gt(n4,n1). % 17.60/17.77 gt(n5,n1). % 17.60/17.77 gt(n999,n1). % 17.60/17.77 gt(n2,n1). % 17.60/17.77 gt(n3,n1). % 17.60/17.77 gt(n4,n2). % 17.60/17.77 gt(n5,n2). % 17.60/17.77 gt(n999,n2). % 17.60/17.77 gt(n3,n2). % 17.60/17.77 gt(n4,n3). % 17.60/17.77 gt(n5,n3). % 17.60/17.77 gt(n999,n3). % 17.60/17.77 all X (le_q(n0,X)&le_q(X,n4)->X=n0|X=n1|X=n2|X=n3|X=n4). % 17.60/17.77 all X (le_q(n0,X)&le_q(X,n5)->X=n0|X=n1|X=n2|X=n3|X=n4|X=n5). % 17.60/17.77 all X (le_q(n0,X)&le_q(X,n0)->X=n0). % 17.60/17.77 all X (le_q(n0,X)&le_q(X,n1)->X=n0|X=n1). % 17.60/17.77 all X (le_q(n0,X)&le_q(X,n2)->X=n0|X=n1|X=n2). % 17.60/17.77 all X (le_q(n0,X)&le_q(X,n3)->X=n0|X=n1|X=n2|X=n3). % 17.60/17.77 succ(succ(succ(succ(n0))))=n4. % 17.60/17.77 succ(succ(succ(succ(succ(n0)))))=n5. % 17.60/17.77 succ(n0)=n1. % 17.60/17.77 succ(succ(n0))=n2. % 17.60/17.77 succ(succ(succ(n0)))=n3. % 17.60/17.77 end_of_list. % 17.60/17.77 % 17.60/17.77 Search stopped in tp_alloc by max_mem option. % 17.60/17.77 % 17.60/17.77 ============ end of search ============ % 17.60/17.77 % 17.60/17.77 -------------- statistics ------------- % 17.60/17.77 clauses given 0 % 17.60/17.77 clauses generated 0 % 17.60/17.77 clauses kept 0 % 17.60/17.77 clauses forward subsumed 0 % 17.60/17.77 clauses back subsumed 0 % 17.60/17.77 Kbytes malloced 11718 % 17.60/17.77 % 17.60/17.77 ----------- times (seconds) ----------- % 17.60/17.77 user CPU time 15.12 (0 hr, 0 min, 15 sec) % 17.60/17.77 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 17.60/17.77 wall-clock time 17 (0 hr, 0 min, 17 sec) % 17.60/17.77 % 17.60/17.77 Process 28000 finished Wed Jul 27 05:01:05 2022 % 17.60/17.77 Otter interrupted % 17.60/17.77 PROOF NOT FOUND %------------------------------------------------------------------------------