Bob is nice. Dave is nice. Erin is quiet. Harry is nice. If someone is quiet and cold then they are green. All quiet people are green.
Bob is nice.
("Bob" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If someone is quiet and cold then they are green.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Harry is nice.
True
1
proof
[(triple4)]
("Harry" "is" "nice" "+")
triple4
Dave is not nice.
False
1
inv-proof
[(triple2)]
("Dave" "is" "nice" "-")
triple2
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is nice.[(triple1)] Dave is nice.[(triple2)] Erin is quiet.[(triple3)] Harry is nice.[(triple4)] @1: Erin is green.[(((triple3) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1