Bob is kind. Charlie is kind. Charlie is smart. Erin is nice. Harry is kind. Harry is nice. Harry is red. If something is nice then it is red. If Bob is red then Bob is cold.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Bob is red then Bob is cold.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "cold" "+"))
Harry is kind.
True
1
proof
[(triple5)]
("Harry" "is" "kind" "+")
triple5
Charlie is not kind.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "kind" "-")
triple2
Bob is not cold.
Unknown
inv-rconc
[@2: Bob is cold.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is kind.[(triple1)] Charlie is kind.[(triple2)] Charlie is smart.[(triple3)] Erin is nice.[(triple4)] Harry is kind.[(triple5)] Harry is nice.[(triple6)] Harry is red.[(triple7 OR ((triple6) -> rule1))] @1: Erin is red.[(((triple4) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
((triple6) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple4) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1