#-------------------------------------------------------------------------- # File : SYN067-3 : TPTP v2.1.0. Released v1.2.0. # Domain : Syntactic # Problem : Pelletier Problem 38 # Version : Special. # Theorem formulation : Different clausification. # English : # Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au # Source : [TPTP] # Names : # Status : unsatisfiable # Rating : 0.75 v2.1.0, 0.00 v2.0.0 # Syntax : Number of clauses : 46 ( 40 non-Horn; 1 unit; 19 RR) # Number of literals : 259 ( 0 equality) # Maximal clause size : 7 ( 5 average) # Number of predicates : 2 ( 0 propositional; 1-2 arity) # Number of functors : 11 ( 5 constant; 0-1 arity) # Number of variables : 120 ( 0 singleton) # Maximal term depth : 2 ( 1 average) # Comments : A full predicate logic version of Pelletier 17 and 33. # : Created using the TPTP clausifier in Otter mode. # : tptp2X -f setheo:sign -t rm_equality:rstfp SYN067-3.p #-------------------------------------------------------------------------- # pel38_1, conjecture. big_p(A); big_p(B); big_p(sk1(B)); big_p(sk3(A)) <- big_p(a). # pel38_2, conjecture. big_p(C); big_p(D); big_p(sk1(D)); big_r(C, sk4(C)) <- big_p(a). # pel38_3, conjecture. big_p(E); big_p(F); big_p(sk1(F)); big_r(sk4(E), sk3(E)) <- big_p(a). # pel38_4, conjecture. big_p(G); big_p(H); big_p(sk3(G)); big_r(H, sk2(H)) <- big_p(a). # pel38_5, conjecture. big_p(I); big_p(J); big_r(I, sk4(I)); big_r(J, sk2(J)) <- big_p(a). # pel38_6, conjecture. big_p(K); big_p(L); big_r(L, sk2(L)); big_r(sk4(K), sk3(K)) <- big_p(a). # pel38_7, conjecture. big_p(M); big_p(sk1(M)); big_p(sk5(N)) <- big_p(O), big_p(a), big_r(N, O). # pel38_8, conjecture. big_p(P); big_p(sk1(P)); big_r(Q, sk6(Q)) <- big_p(R), big_p(a), big_r(Q, R). # pel38_9, conjecture. big_p(S); big_p(sk1(S)); big_r(sk6(T), sk5(T)) <- big_p(U), big_p(a), big_r(T, U). # pel38_10, conjecture. big_p(V); big_p(sk5(W)); big_r(V, sk2(V)) <- big_p(X), big_p(a), big_r(W, X). # pel38_11, conjecture. big_p(Y); big_r(Z, sk6(Z)); big_r(Y, sk2(Y)) <- big_p(A1), big_p(a), big_r(Z, A1). # pel38_12, conjecture. big_p(B1); big_r(B1, sk2(B1)); big_r(sk6(C1), sk5(C1)) <- big_p(D1), big_p(a), big_r(C1, D1). # pel38_13, conjecture. big_p(E1); big_p(F1); big_p(sk3(E1)); big_r(sk2(F1), sk1(F1)) <- big_p(a). # pel38_14, conjecture. big_p(G1); big_p(H1); big_r(G1, sk4(G1)); big_r(sk2(H1), sk1(H1)) <- big_p(a). # pel38_15, conjecture. big_p(I1); big_p(J1); big_r(sk2(J1), sk1(J1)); big_r(sk4(I1), sk3(I1)) <- big_p(a). # pel38_16, conjecture. big_p(K1); big_p(sk1(L1)); big_p(sk3(K1)) <- big_p(M1), big_p(a), big_r(L1, M1). # pel38_17, conjecture. big_p(N1); big_p(sk3(N1)); big_r(O1, sk2(O1)) <- big_p(P1), big_p(a), big_r(O1, P1). # pel38_18, conjecture. big_p(Q1); big_p(sk1(R1)); big_r(Q1, sk4(Q1)) <- big_p(S1), big_p(a), big_r(R1, S1). # pel38_19, conjecture. big_p(T1); big_r(T1, sk4(T1)); big_r(U1, sk2(U1)) <- big_p(V1), big_p(a), big_r(U1, V1). # pel38_20, conjecture. big_p(W1); big_p(sk3(W1)); big_r(sk2(X1), sk1(X1)) <- big_p(Y1), big_p(a), big_r(X1, Y1). # pel38_21, conjecture. big_p(Z1); big_r(Z1, sk4(Z1)); big_r(sk2(A2), sk1(A2)) <- big_p(B2), big_p(a), big_r(A2, B2). # pel38_22, conjecture. big_p(C2); big_p(sk1(D2)); big_r(sk4(C2), sk3(C2)) <- big_p(E2), big_p(a), big_r(D2, E2). # pel38_23, conjecture. big_p(F2); big_r(G2, sk2(G2)); big_r(sk4(F2), sk3(F2)) <- big_p(H2), big_p(a), big_r(G2, H2). # pel38_24, conjecture. big_p(I2); big_r(sk2(J2), sk1(J2)); big_r(sk4(I2), sk3(I2)) <- big_p(K2), big_p(a), big_r(J2, K2). # pel38_25, conjecture. big_p(L2); big_p(sk5(M2)); big_r(sk2(L2), sk1(L2)) <- big_p(N2), big_p(a), big_r(M2, N2). # pel38_26, conjecture. big_p(O2); big_r(P2, sk6(P2)); big_r(sk2(O2), sk1(O2)) <- big_p(Q2), big_p(a), big_r(P2, Q2). # pel38_27, conjecture. big_p(R2); big_r(sk2(R2), sk1(R2)); big_r(sk6(S2), sk5(S2)) <- big_p(T2), big_p(a), big_r(S2, T2). # pel38_28, conjecture. big_p(sk1(U2)); big_p(sk5(V2)) <- big_p(W2), big_p(X2), big_p(a), big_r(V2, W2), big_r(U2, X2). # pel38_29, conjecture. big_p(sk5(Y2)); big_r(Z2, sk2(Z2)) <- big_p(A3), big_p(B3), big_p(a), big_r(Y2, A3), big_r(Z2, B3). # pel38_30, conjecture. big_p(sk1(C3)); big_r(D3, sk6(D3)) <- big_p(E3), big_p(F3), big_p(a), big_r(D3, E3), big_r(C3, F3). # pel38_31, conjecture. big_r(G3, sk6(G3)); big_r(H3, sk2(H3)) <- big_p(I3), big_p(J3), big_p(a), big_r(G3, I3), big_r(H3, J3). # pel38_32, conjecture. big_p(sk5(K3)); big_r(sk2(L3), sk1(L3)) <- big_p(M3), big_p(N3), big_p(a), big_r(K3, M3), big_r(L3, N3). # pel38_33, conjecture. big_r(O3, sk6(O3)); big_r(sk2(P3), sk1(P3)) <- big_p(Q3), big_p(R3), big_p(a), big_r(O3, Q3), big_r(P3, R3). # pel38_34, conjecture. big_p(sk1(S3)); big_r(sk6(T3), sk5(T3)) <- big_p(U3), big_p(V3), big_p(a), big_r(T3, U3), big_r(S3, V3). # pel38_35, conjecture. big_r(W3, sk2(W3)); big_r(sk6(X3), sk5(X3)) <- big_p(Y3), big_p(Z3), big_p(a), big_r(X3, Y3), big_r(W3, Z3). # pel38_36, conjecture. big_r(sk2(A4), sk1(A4)); big_r(sk6(B4), sk5(B4)) <- big_p(C4), big_p(D4), big_p(a), big_r(B4, C4), big_r(A4, D4). # pel38_37, conjecture. big_p(a) <- . # pel38_38, conjecture. big_p(sk10); big_p(sk8) <- big_p(sk7), big_p(sk9). # pel38_39, conjecture. big_p(sk8); big_r(sk9, sk10) <- big_p(sk7), big_p(sk9). # pel38_40, conjecture. big_p(sk10); big_r(sk7, sk8) <- big_p(sk7), big_p(sk9). # pel38_41, conjecture. big_r(sk7, sk8); big_r(sk9, sk10) <- big_p(sk7), big_p(sk9). # pel38_42, conjecture. big_p(sk8) <- big_p(E4), big_p(sk7), big_r(F4, E4), big_r(sk9, F4). # pel38_43, conjecture. big_r(sk7, sk8) <- big_p(G4), big_p(sk7), big_r(H4, G4), big_r(sk9, H4). # pel38_44, conjecture. big_p(sk10) <- big_p(I4), big_p(sk9), big_r(J4, I4), big_r(sk7, J4). # pel38_45, conjecture. big_r(sk9, sk10) <- big_p(K4), big_p(sk9), big_r(L4, K4), big_r(sk7, L4). # pel38_46, conjecture. <- big_p(M4), big_p(N4), big_r(O4, M4), big_r(P4, N4), big_r(sk7, P4), big_r(sk9, O4). #--------------------------------------------------------------------------