============================================================================== This session transcript shows the output of show_frontiers/2 (from show_frontiers.pl) for a proof of problem 'LCL082-1' (goal "Simp" from axiom "Lukasiewiz") with different formatting options. ============================================================================== ?- show_frontiers('LCL082-1', [globalvars]). ------------------------------------------------------------------------------ Proof of LCL082-1; c/t/h-size: 6/7/6; prover: 20220411_5808 Axiom 1: i(i(i(A,B),C),i(i(C,A),i(D,A))) ------------------------------------------------------------------------------ 1. init [i(a,i(b,a))] 2. d [i(A,i(a,i(b,a))), A] 3. d [i(B,i(A,i(a,i(b,a)))), B, A] nonfrag [i(i(i(b,a),C),D), i(D,i(b,a))] 4. d [i(C,i(B,i(A,i(a,i(b,a))))), C, B, A] nonfrag [i(D,i(C,i(B,i(A,i(a,i(b,a)))))), D, C, B, A] 5. axiom(1) [i(i(i(a,i(b,a)),D),E), i(E,i(a,i(b,a))), A] nonfrag [i(F,i(i(i(a,i(b,a)),D),E)), F, i(E,i(a,i(b,a))), A] 6. axiom(1) [i(i(i(D,a),i(F,a)),i(a,i(b,a))), A] 7. d [i(G,i(i(i(D,a),i(F,a)),i(a,i(b,a)))), G, A] nonfrag [i(i(i(b,a),H),i(D,a)), A] 8. d [i(H,i(G,i(i(i(D,a),i(F,a)),i(a,i(b,a))))), H, G, A] nonfrag [i(i(i(a,i(b,a)),I),J), i(J,i(a,i(b,a))), A] 9. d [i(I,i(H,i(G,i(i(i(D,a),i(F,a)),i(a,i(b,a)))))), I, H, G, A] nonfrag [i(J,i(I,i(H,i(G,i(i(i(D,a),i(F,a)),i(a,i(b,a))))))), J, I, H, G, A] 10. axiom(1) [i(i(i(i(i(D,a),i(F,a)),i(a,i(b,a))),J),K), i(K,i(i(i(D,a),i(F,a)),i(a,i(b,a)))), G, A] nonfrag [i(i(i(J,i(i(D,a),i(F,a))),i(L,i(i(D,a),i(F,a)))),i(i(i(D,a),i(F,a)),i(a,i(b,a)))), G, A] 11. d [i(L,i(i(i(i(i(D,a),i(F,a)),i(a,i(b,a))),J),K)), L, i(K,i(i(i(D,a),i(F,a)),i(a,i(b,a)))), G, A] nonfrag [i(M,i(L,i(i(i(i(i(D,a),i(F,a)),i(a,i(b,a))),J),K))), M, L, i(K,i(i(i(D,a),i(F,a)),i(a,i(b,a)))), G, A] 12. axiom(1) [i(i(J,M),i(i(i(D,a),i(F,a)),i(a,i(b,a)))), i(i(N,J),i(i(i(D,a),i(F,a)),i(a,i(b,a)))), G, A] nonfrag [i(O,i(i(J,M),i(i(i(D,a),i(F,a)),i(a,i(b,a))))), O, i(i(N,J),i(i(i(D,a),i(F,a)),i(a,i(b,a)))), G, A] 13. axiom(1) [i(i(N,i(i(b,a),O)),i(i(i(D,a),i(b,a)),i(a,i(b,a)))), G, A] nonfrag [i(P,i(i(N,i(i(b,a),O)),i(i(i(D,a),i(b,a)),i(a,i(b,a))))), P, G, A] 14. axiom(1) [G, A] nonfrag [i(P,G), P, A] 15. axiom(1) [A] nonfrag [i(P,A), P] 16. axiom(1) [] true. ?- show_frontiers('LCL082-1', [globalvars,firstonly]). ------------------------------------------------------------------------------ Proof of LCL082-1; c/t/h-size: 6/7/6; prover: 20220411_5808 Axiom 1: i(i(i(A,B),C),i(i(C,A),i(D,A))) ------------------------------------------------------------------------------ 1. init i(a,i(b,a)) 2. d i(A,i(a,i(b,a))) 3. d i(B,i(A,i(a,i(b,a)))) nonfrag i(i(i(b,a),C),D) 4. d i(C,i(B,i(A,i(a,i(b,a))))) nonfrag i(D,i(C,i(B,i(A,i(a,i(b,a)))))) 5. axiom(1) i(i(i(a,i(b,a)),D),E) nonfrag i(F,i(i(i(a,i(b,a)),D),E)) 6. axiom(1) i(i(i(D,a),i(F,a)),i(a,i(b,a))) 7. d i(G,i(i(i(D,a),i(F,a)),i(a,i(b,a)))) nonfrag i(i(i(b,a),H),i(D,a)) 8. d i(H,i(G,i(i(i(D,a),i(F,a)),i(a,i(b,a))))) nonfrag i(i(i(a,i(b,a)),I),J) 9. d i(I,i(H,i(G,i(i(i(D,a),i(F,a)),i(a,i(b,a)))))) nonfrag i(J,i(I,i(H,i(G,i(i(i(D,a),i(F,a)),i(a,i(b,a))))))) 10. axiom(1) i(i(i(i(i(D,a),i(F,a)),i(a,i(b,a))),J),K) nonfrag i(i(i(J,i(i(D,a),i(F,a))),i(L,i(i(D,a),i(F,a)))),i(i(i(D,a),i(F,a)),i(a,i(b,a)))) 11. d i(L,i(i(i(i(i(D,a),i(F,a)),i(a,i(b,a))),J),K)) nonfrag i(M,i(L,i(i(i(i(i(D,a),i(F,a)),i(a,i(b,a))),J),K))) 12. axiom(1) i(i(J,M),i(i(i(D,a),i(F,a)),i(a,i(b,a)))) nonfrag i(O,i(i(J,M),i(i(i(D,a),i(F,a)),i(a,i(b,a))))) 13. axiom(1) i(i(N,i(i(b,a),O)),i(i(i(D,a),i(b,a)),i(a,i(b,a)))) nonfrag i(P,i(i(N,i(i(b,a),O)),i(i(i(D,a),i(b,a)),i(a,i(b,a))))) 14. axiom(1) G nonfrag i(P,G) 15. axiom(1) A nonfrag i(P,A) true. ?- show_frontiers('LCL082-1', [cfterms([j,k,m,n,o,p,q,r,s,t,u,v,w,x,y,z]),globalvars]). ------------------------------------------------------------------------------ Proof of LCL082-1; c/t/h-size: 6/7/6; prover: 20220411_5808 Axiom 1: CCCjkmCCmjCnj ------------------------------------------------------------------------------ 1. init [CaCba] 2. d [CjCaCba, j] 3. d [CkCjCaCba, k, j] nonfrag [CCCbamn, CnCba] 4. d [CmCkCjCaCba, m, k, j] nonfrag [CnCmCkCjCaCba, n, m, k, j] 5. axiom(1) [CCCaCbano, CoCaCba, j] nonfrag [CpCCCaCbano, p, CoCaCba, j] 6. axiom(1) [CCCnaCpaCaCba, j] 7. d [CqCCCnaCpaCaCba, q, j] nonfrag [CCCbarCna, j] 8. d [CrCqCCCnaCpaCaCba, r, q, j] nonfrag [CCCaCbast, CtCaCba, j] 9. d [CsCrCqCCCnaCpaCaCba, s, r, q, j] nonfrag [CtCsCrCqCCCnaCpaCaCba, t, s, r, q, j] 10. axiom(1) [CCCCCnaCpaCaCbatu, CuCCCnaCpaCaCba, q, j] nonfrag [CCCtCCnaCpaCvCCnaCpaCCCnaCpaCaCba, q, j] 11. d [CvCCCCCnaCpaCaCbatu, v, CuCCCnaCpaCaCba, q, j] nonfrag [CwCvCCCCCnaCpaCaCbatu, w, v, CuCCCnaCpaCaCba, q, j] 12. axiom(1) [CCtwCCCnaCpaCaCba, CCxtCCCnaCpaCaCba, q, j] nonfrag [CyCCtwCCCnaCpaCaCba, y, CCxtCCCnaCpaCaCba, q, j] 13. axiom(1) [CCxCCbayCCCnaCbaCaCba, q, j] nonfrag [CzCCxCCbayCCCnaCbaCaCba, z, q, j] 14. axiom(1) [q, j] nonfrag [Czq, z, j] 15. axiom(1) [j] nonfrag [Czj, z] 16. axiom(1) [] true. ?- show_frontiers('LCL082-1', [cfterms,blankvars]). ------------------------------------------------------------------------------ Proof of LCL082-1; c/t/h-size: 6/7/6; prover: 20220411_5808 Axiom 1: CCCpqrCCrpCsp ------------------------------------------------------------------------------ 1. init [CaCba] 2. d [C_CaCba, _] 3. d [C_C_CaCba, _, _] nonfrag [CCCba__, C_Cba] 4. d [C_C_C_CaCba, _, _, _] nonfrag [C_C_C_C_CaCba, _, _, _, _] 5. axiom(1) [CCCaCba__, C_CaCba, _] nonfrag [C_CCCaCba__, _, C_CaCba, _] 6. axiom(1) [CCC_aC_aCaCba, _] 7. d [C_CCC_aC_aCaCba, _, _] nonfrag [CCCba_C_a, _] 8. d [C_C_CCC_aC_aCaCba, _, _, _] nonfrag [CCCaCba__, C_CaCba, _] 9. d [C_C_C_CCC_aC_aCaCba, _, _, _, _] nonfrag [C_C_C_C_CCC_aC_aCaCba, _, _, _, _, _] 10. axiom(1) [CCCCC_aC_aCaCba__, C_CCC_aC_aCaCba, _, _] nonfrag [CCC_CC_aC_aC_CC_aC_aCCC_aC_aCaCba, _, _] 11. d [C_CCCCC_aC_aCaCba__, _, C_CCC_aC_aCaCba, _, _] nonfrag [C_C_CCCCC_aC_aCaCba__, _, _, C_CCC_aC_aCaCba, _, _] 12. axiom(1) [CC__CCC_aC_aCaCba, CC__CCC_aC_aCaCba, _, _] nonfrag [C_CC__CCC_aC_aCaCba, _, CC__CCC_aC_aCaCba, _, _] 13. axiom(1) [CC_CCba_CCC_aCbaCaCba, _, _] nonfrag [C_CC_CCba_CCC_aCbaCaCba, _, _, _] 14. axiom(1) [_, _] nonfrag [C__, _, _] 15. axiom(1) [_] nonfrag [C__, _] 16. axiom(1) [] true.