Anne is young. Bob is smart. Gary is cold. Harry is cold. Harry is furry. Harry is nice. Harry is young. If Harry is cold then Harry is furry. If Bob is big and Bob is red then Bob is furry. Smart, cold people are red.
Anne is young.
("Anne" "is" "young" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is cold then Harry is furry.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "furry" "+"))
If Bob is big and Bob is red then Bob is furry.
((("Bob" "is" "big" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "furry" "+"))
Smart, cold people are red.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Gary is cold.
True
1
proof
[(triple3)]
("Gary" "is" "cold" "+")
triple3
Harry is not nice.
False
1
inv-proof
[(triple6)]
("Harry" "is" "nice" "-")
triple6
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "red" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Anne is young.[(triple1)] Bob is smart.[(triple2)] Gary is cold.[(triple3)] Harry is cold.[(triple4)] Harry is furry.[(triple5 OR ((triple4) -> rule1))] Harry is nice.[(triple6)] Harry is young.[(triple7)]
Anne is young.
("Anne" "is" "young" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
triple5
((triple4) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7