Bob is furry. Bob is kind. Gary is cold. All kind, furry things are nice. All kind things are furry. All kind, nice things are young.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Gary is cold.
("Gary" "is" "cold" "+")
All kind, furry things are nice.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
All kind, nice things are young.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Bob is furry.
True
1
proof
[(triple1 OR ((triple2) -> rule2))]
("Bob" "is" "furry" "+")
triple1
((triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule2))]
("Bob" "is" "furry" "-")
triple1
((triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
True
3
proof
[(((triple2 triple1) -> rule1) OR ((triple2 ((triple2) -> rule2)) -> rule1))]
("Bob" "is" "nice" "+")
((triple2 triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((triple2 triple1) -> rule1) OR ((triple2 ((triple2) -> rule2)) -> rule1))]
("Bob" "is" "nice" "-")
((triple2 triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
True
5
proof
[(((triple2 ((triple2 triple1) -> rule1)) -> rule3) OR ((triple2 ((triple2 ((triple2) -> rule2)) -> rule1)) -> rule3))]
("Bob" "is" "young" "+")
((triple2 ((triple2 triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((triple2 ((triple2 ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not young.
False
5
inv-proof
[(((triple2 ((triple2 triple1) -> rule1)) -> rule3) OR ((triple2 ((triple2 ((triple2) -> rule2)) -> rule1)) -> rule3))]
("Bob" "is" "young" "-")
((triple2 ((triple2 triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((triple2 ((triple2 ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "young" "+")
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "nice" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Bob is furry.[(triple1 OR ((triple2) -> rule2))] Bob is kind.[(triple2)] Gary is cold.[(triple3)] @1: Bob is nice.[(((triple2 triple1) -> rule1) OR ((triple2 ((triple2) -> rule2)) -> rule1))] @2: Bob is young.[(((triple2 ((triple2 triple1) -> rule1)) -> rule3) OR ((triple2 ((triple2 ((triple2) -> rule2)) -> rule1)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
((triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
((triple2 triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple2 ((triple2 triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((triple2 ((triple2 ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3