============================================================================== This session transcript shows the output of show_frontiers/2 (from show_frontiers.pl) for a proof of problem 'LCL044-1' with different formatting options. ============================================================================== ?- show_frontiers('LCL044-1', [globalvars]). ------------------------------------------------------------------------------ Proof of LCL044-1; c/t/h-size: 3/3/3; prover: 20220411_5808 Axiom 1: i(A,i(n(A),B)) Axiom 2: i(A,i(B,A)) Axiom 3: i(i(A,i(B,C)),i(B,i(A,C))) Axiom 4: i(i(A,B),i(i(C,A),i(C,B))) Axiom 5: i(i(A,B),i(i(n(A),B),B)) ------------------------------------------------------------------------------ 1. init [i(a,n(n(a)))] 2. d [i(A,i(a,n(n(a)))), A] nonfrag [n(n(a))] 3. d [i(B,i(A,i(a,n(n(a))))), B, A] nonfrag [i(C,i(B,i(A,i(a,n(n(a)))))), C, B, A] nonfrag [B, n(B)] nonfrag [i(a,n(n(a))), A] nonfrag [i(a,i(A,n(n(a)))), A] nonfrag [i(C,n(n(a))), i(a,C)] 4. axiom(5) [i(C,i(a,n(n(a)))), i(n(C),i(a,n(n(a))))] nonfrag [i(n(n(n(a))),i(a,n(n(a))))] 5. d [i(D,i(C,i(a,n(n(a))))), D, i(n(C),i(a,n(n(a))))] nonfrag [i(E,i(D,i(C,i(a,n(n(a)))))), E, D, i(n(C),i(a,n(n(a))))] nonfrag [D, i(n(n(D)),i(a,n(n(a))))] nonfrag [i(a,n(n(a))), i(n(C),i(a,n(n(a))))] nonfrag [i(E,n(n(a))), i(n(i(a,E)),i(a,n(n(a))))] nonfrag [i(E,i(a,n(n(a)))), i(n(i(n(E),i(a,n(n(a))))),i(a,n(n(a))))] 6. axiom(3) [i(a,i(C,n(n(a)))), i(n(C),i(a,n(n(a))))] nonfrag [i(E,i(a,i(C,n(n(a))))), E, i(n(C),i(a,n(n(a))))] 7. axiom(1) [i(n(n(a)),i(a,n(n(a))))] nonfrag [i(E,i(n(n(a)),i(a,n(n(a))))), E] 8. axiom(2) [] true. ?- show_frontiers('LCL044-1', [globalvars,firstonly]). ------------------------------------------------------------------------------ Proof of LCL044-1; c/t/h-size: 3/3/3; prover: 20220411_5808 Axiom 1: i(A,i(n(A),B)) Axiom 2: i(A,i(B,A)) Axiom 3: i(i(A,i(B,C)),i(B,i(A,C))) Axiom 4: i(i(A,B),i(i(C,A),i(C,B))) Axiom 5: i(i(A,B),i(i(n(A),B),B)) ------------------------------------------------------------------------------ 1. init i(a,n(n(a))) 2. d i(A,i(a,n(n(a)))) nonfrag n(n(a)) 3. d i(B,i(A,i(a,n(n(a))))) nonfrag i(C,i(B,i(A,i(a,n(n(a)))))) nonfrag B nonfrag i(a,n(n(a))) nonfrag i(a,i(A,n(n(a)))) nonfrag i(C,n(n(a))) 4. axiom(5) i(C,i(a,n(n(a)))) nonfrag i(n(n(n(a))),i(a,n(n(a)))) 5. d i(D,i(C,i(a,n(n(a))))) nonfrag i(E,i(D,i(C,i(a,n(n(a)))))) nonfrag D nonfrag i(a,n(n(a))) nonfrag i(E,n(n(a))) nonfrag i(E,i(a,n(n(a)))) 6. axiom(3) i(a,i(C,n(n(a)))) nonfrag i(E,i(a,i(C,n(n(a))))) 7. axiom(1) i(n(n(a)),i(a,n(n(a)))) nonfrag i(E,i(n(n(a)),i(a,n(n(a))))) true. ?- show_frontiers('LCL044-1', [cfterms,globalvars]). ------------------------------------------------------------------------------ Proof of LCL044-1; c/t/h-size: 3/3/3; prover: 20220411_5808 Axiom 1: CpCNpq Axiom 2: CpCqp Axiom 3: CCpCqrCqCpr Axiom 4: CCpqCCrpCrq Axiom 5: CCpqCCNpqq ------------------------------------------------------------------------------ 1. init [CaNNa] 2. d [CpCaNNa, p] nonfrag [NNa] 3. d [CqCpCaNNa, q, p] nonfrag [CrCqCpCaNNa, r, q, p] nonfrag [q, Nq] nonfrag [CaNNa, p] nonfrag [CaCpNNa, p] nonfrag [CrNNa, Car] 4. axiom(5) [CrCaNNa, CNrCaNNa] nonfrag [CNNNaCaNNa] 5. d [CsCrCaNNa, s, CNrCaNNa] nonfrag [CtCsCrCaNNa, t, s, CNrCaNNa] nonfrag [s, CNNsCaNNa] nonfrag [CaNNa, CNrCaNNa] nonfrag [CtNNa, CNCatCaNNa] nonfrag [CtCaNNa, CNCNtCaNNaCaNNa] 6. axiom(3) [CaCrNNa, CNrCaNNa] nonfrag [CtCaCrNNa, t, CNrCaNNa] 7. axiom(1) [CNNaCaNNa] nonfrag [CtCNNaCaNNa, t] 8. axiom(2) [] true. ?- show_frontiers('LCL044-1', [cfterms,blankvars]). ------------------------------------------------------------------------------ Proof of LCL044-1; c/t/h-size: 3/3/3; prover: 20220411_5808 Axiom 1: CpCNpq Axiom 2: CpCqp Axiom 3: CCpCqrCqCpr Axiom 4: CCpqCCrpCrq Axiom 5: CCpqCCNpqq ------------------------------------------------------------------------------ 1. init [CaNNa] 2. d [C_CaNNa, _] nonfrag [NNa] 3. d [C_C_CaNNa, _, _] nonfrag [C_C_C_CaNNa, _, _, _] nonfrag [_, N_] nonfrag [CaNNa, _] nonfrag [CaC_NNa, _] nonfrag [C_NNa, Ca_] 4. axiom(5) [C_CaNNa, CN_CaNNa] nonfrag [CNNNaCaNNa] 5. d [C_C_CaNNa, _, CN_CaNNa] nonfrag [C_C_C_CaNNa, _, _, CN_CaNNa] nonfrag [_, CNN_CaNNa] nonfrag [CaNNa, CN_CaNNa] nonfrag [C_NNa, CNCa_CaNNa] nonfrag [C_CaNNa, CNCN_CaNNaCaNNa] 6. axiom(3) [CaC_NNa, CN_CaNNa] nonfrag [C_CaC_NNa, _, CN_CaNNa] 7. axiom(1) [CNNaCaNNa] nonfrag [C_CNNaCaNNa, _] 8. axiom(2) [] true.