Anne is blue. Anne is kind. Anne is nice. Anne is smart. Charlie is blue. Gary is furry. Harry is big. Kind things are blue. If Harry is smart and Harry is big then Harry is nice. If something is smart then it is nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is big.
("Harry" "is" "big" "+")
Kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If Harry is smart and Harry is big then Harry is nice.
((("Harry" "is" "smart" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "nice" "+"))
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Anne is smart.
True
1
proof
[(triple4)]
("Anne" "is" "smart" "+")
triple4
Harry is not big.
False
1
inv-proof
[(triple7)]
("Harry" "is" "big" "-")
triple7
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is blue.[(triple1 OR ((triple2) -> rule1))] Anne is kind.[(triple2)] Anne is nice.[(triple3 OR ((triple4) -> rule3))] Anne is smart.[(triple4)] Charlie is blue.[(triple5)] Gary is furry.[(triple6)] Harry is big.[(triple7)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple2) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple4) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7