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