Bob is furry. Erin is blue. Gary is round. If something is furry then it is kind. All kind things are green. Kind, furry things are round.
Bob is furry.
("Bob" "is" "furry" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is furry then it is kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Kind, furry things are round.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Erin is blue.
True
1
proof
[(triple2)]
("Erin" "is" "blue" "+")
triple2
Gary is not round.
False
1
inv-proof
[(triple3)]
("Gary" "is" "round" "-")
triple3
Bob is kind.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "kind" "-")
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not green.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "green" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is green.
Unknown
rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Erin" "is" "green" "+")
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "kind" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is furry.[(triple1)] Erin is blue.[(triple2)] Gary is round.[(triple3)] @1: Bob is kind.[(((triple1) -> rule1))] @2: Bob is green.[(((((triple1) -> rule1)) -> rule2))] Bob is round.[(((((triple1) -> rule1) triple1) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2