A Sample Session with the LJFOL Prover

Below is a sample session using Terzo to load and then run the prover in this collection. The input of the user is in red.

miller:examples/ljfol >~/terzo/bin/Terzo
loading /share/pub/miller/terzo/bin/.lpsml ......................... done
Terzo lambda-Prolog, Version 1.0b, Built Tue Jul 16 15:52:11 EDT 1996
[reading file /share/pub/miller/terzo/lib/terzo.rc]
[closed file /share/pub/miller/terzo/lib/terzo.rc]
Terzo> #load "go".
[reading file ./go]
[reading file /share/pub/miller/terzo/doc/SystemModules/maps.mod]
module maps
[closed file /share/pub/miller/terzo/doc/SystemModules/maps.mod]
[reading file /share/pub/miller/terzo/lib/list_util.mod]
module ListUtil
[closed file /share/pub/miller/terzo/lib/list_util.mod]
[reading file /share/pub/miller/elios/lProlog/examples/utilities/control.mod]
module control
[closed file /share/pub/miller/elios/lProlog/examples/utilities/control.mod]
[reading file /share/pub/miller/elios/lProlog/examples/utilities/lists.mod]
module lists
[closed file /share/pub/miller/elios/lProlog/examples/utilities/lists.mod]
[reading file /share/pub/miller/elios/lProlog/examples/utilities/alist.mod]
module Alist
[closed file /share/pub/miller/elios/lProlog/examples/utilities/alist.mod]
[reading file /share/pub/miller/elios/lProlog/examples/tactics/goals.mod]
module goals
[closed file /share/pub/miller/elios/lProlog/examples/tactics/goals.mod]
[reading file /share/pub/miller/elios/lProlog/examples/tactics/goalred.mod]
module goalred
[closed file /share/pub/miller/elios/lProlog/examples/tactics/goalred.mod]
[reading file /share/pub/miller/elios/lProlog/examples/tactics/maptac.mod]
module maptac
[closed file /share/pub/miller/elios/lProlog/examples/tactics/maptac.mod]
[reading file /share/pub/miller/elios/lProlog/examples/tactics/tacticals.mod]
module tacticals
[closed file /share/pub/miller/elios/lProlog/examples/tactics/tacticals.mod]
[reading file /share/pub/miller/elios/lProlog/examples/tactics/inter_tacs.mod]
module inter_tacs
[closed file /share/pub/miller/elios/lProlog/examples/tactics/inter_tacs.mod]
[reading file /share/pub/miller/elios/lProlog/examples/ljfol/fol.mod]
module fol
[closed file /share/pub/miller/elios/lProlog/examples/ljfol/fol.mod]
[reading file /share/pub/miller/elios/lProlog/examples/ljfol/printer.mod]
module printer
[closed file /share/pub/miller/elios/lProlog/examples/ljfol/printer.mod]
[reading file /share/pub/miller/elios/lProlog/examples/ljfol/scanner.mod]
module scanner
[closed file /share/pub/miller/elios/lProlog/examples/ljfol/scanner.mod]
[reading file /share/pub/miller/elios/lProlog/examples/ljfol/parser.mod]
module parser
[closed file /share/pub/miller/elios/lProlog/examples/ljfol/parser.mod]
[reading file /share/pub/miller/elios/lProlog/examples/ljfol/formulas.mod]
module formulas
[closed file /share/pub/miller/elios/lProlog/examples/ljfol/formulas.mod]
[reading file /share/pub/miller/elios/lProlog/examples/ljfol/lj.mod]
module lj
[closed file /share/pub/miller/elios/lProlog/examples/ljfol/lj.mod]
[reading file /share/pub/miller/elios/lProlog/examples/ljfol/rules.mod]
module rules
[closed file /share/pub/miller/elios/lProlog/examples/ljfol/rules.mod]
[reading file /share/pub/miller/elios/lProlog/examples/ljfol/top.mod]
module top
[closed file /share/pub/miller/elios/lProlog/examples/ljfol/top.mod]
[closed file ./go]
Terzo> #query top prover.
The following formulas are available for proving:
distrib_quant1 distrib_quant2 distrib_quant3 cases1 cases2 cases3 bugs blocks baffler modus_quant primes reflexive quant_equiv 
Enter a formula name: blocks.
-----------------------------------
(((((((forall x ((blue x) => (neg (green x)))) and (blue c)) and (green a)) and (on_top b c)) and (on_top a b)) and (forall x ((neg (green x)) or (green x)))) => (exists y (exists y1 (((on_top y y1) and (neg (green y1))) and (green y)))))
Enter tactic: go.
(1) (forall x ((blue x) => (neg (green x))))
(2) (blue c)
(3) (green a)
(4) (on_top b c)
(5) (on_top a b)
(6) (forall x ((neg (green x)) or (green x)))
-----------------------------------
(exists y (exists y1 (((on_top y y1) and (neg (green y1))) and (green y))))
Enter tactic: forallq_l 6.
Enter term: b.
(1) ((neg (green b)) or (green b))
(2) (forall x ((blue x) => (neg (green x))))
(3) (blue c)
(4) (green a)
(5) (on_top b c)
(6) (on_top a b)
(7) (forall x ((neg (green x)) or (green x)))
-----------------------------------
(exists y (exists y1 (((on_top y y1) and (neg (green y1))) and (green y))))
Enter tactic: weaken 7.
(1) ((neg (green b)) or (green b))
(2) (forall x ((blue x) => (neg (green x))))
(3) (blue c)
(4) (green a)
(5) (on_top b c)
(6) (on_top a b)
-----------------------------------
(exists y (exists y1 (((on_top y y1) and (neg (green y1))) and (green y))))
Enter tactic: or_l 1.
(1) (neg (green b))
(2) (forall x ((blue x) => (neg (green x))))
(3) (blue c)
(4) (green a)
(5) (on_top b c)
(6) (on_top a b)
-----------------------------------
(exists y (exists y1 (((on_top y y1) and (neg (green y1))) and (green y))))
Enter tactic: existsq_r.
Enter term: a.
(1) (neg (green b))
(2) (forall x ((blue x) => (neg (green x))))
(3) (blue c)
(4) (green a)
(5) (on_top b c)
(6) (on_top a b)
-----------------------------------
(exists y (((on_top a y) and (neg (green y))) and (green a)))
Enter tactic: existsq_r.
Enter term: b.
(1) (neg (green b))
(2) (forall x ((blue x) => (neg (green x))))
(3) (blue c)
(4) (green a)
(5) (on_top b c)
(6) (on_top a b)
-----------------------------------
(((on_top a b) and (neg (green b))) and (green a))
Enter tactic: go.
(1) (green b)
(2) (forall x ((blue x) => (neg (green x))))
(3) (blue c)
(4) (green a)
(5) (on_top b c)
(6) (on_top a b)
-----------------------------------
(exists y (exists y1 (((on_top y y1) and (neg (green y1))) and (green y))))
Enter tactic: existsq_r.
Enter term: b.
(1) (green b)
(2) (forall x ((blue x) => (neg (green x))))
(3) (blue c)
(4) (green a)
(5) (on_top b c)
(6) (on_top a b)
-----------------------------------
(exists y (((on_top b y) and (neg (green y))) and (green b)))
Enter tactic: existsq_r.
Enter term: c.
(1) (green b)
(2) (forall x ((blue x) => (neg (green x))))
(3) (blue c)
(4) (green a)
(5) (on_top b c)
(6) (on_top a b)
-----------------------------------
(((on_top b c) and (neg (green c))) and (green b))
Enter tactic: go.
(1) (green c)
(2) (green b)
(3) (forall x ((blue x) => (neg (green x))))
(4) (blue c)
(5) (green a)
(6) (on_top b c)
(7) (on_top a b)
-----------------------------------
false
Enter tactic: forallq_l 3.
Enter term: 4.
Tactic failed.
(1) (green c)
(2) (green b)
(3) (forall x ((blue x) => (neg (green x))))
(4) (blue c)
(5) (green a)
(6) (on_top b c)
(7) (on_top a b)
-----------------------------------
false
Enter tactic: forallq_l 3.
Enter term: c.
(1) ((blue c) => (neg (green c)))
(2) (green c)
(3) (green b)
(4) (forall x ((blue x) => (neg (green x))))
(5) (blue c)
(6) (green a)
(7) (on_top b c)
(8) (on_top a b)
-----------------------------------
false
Enter tactic: imp_l 1.
(1) ((blue c) => (neg (green c)))
(2) (green c)
(3) (green b)
(4) (forall x ((blue x) => (neg (green x))))
(5) (blue c)
(6) (green a)
(7) (on_top b c)
(8) (on_top a b)
-----------------------------------
(blue c)
Enter tactic: go.
(1) (neg (green c))
(2) (green c)
(3) (green b)
(4) (forall x ((blue x) => (neg (green x))))
(5) (blue c)
(6) (green a)
(7) (on_top b c)
(8) (on_top a b)
-----------------------------------
false
Enter tactic: neg_l 1.
(1) (neg (green c))
(2) (green c)
(3) (green b)
(4) (forall x ((blue x) => (neg (green x))))
(5) (blue c)
(6) (green a)
(7) (on_top b c)
(8) (on_top a b)
-----------------------------------
(green c)
Enter tactic: go.

solved
Terzo>