Bob is furry. Bob is quiet. Bob is red. Bob is smart. Bob is white. Bob is young. Dave is furry. Erin is furry. Erin is red. Erin is white. Harry is quiet. Harry is young. If Dave is kind and Dave is furry then Dave is white. If Bob is quiet then Bob is furry. All kind, young things are red. All smart, young things are kind. Red, kind things are young. All white things are furry. All young, kind things are smart. If Erin is young then Erin is white.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
If Dave is kind and Dave is furry then Dave is white.
((("Dave" "is" "kind" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "white" "+"))
If Bob is quiet then Bob is furry.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "furry" "+"))
All kind, young things are red.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
All smart, young things are kind.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Red, kind things are young.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All white things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
All young, kind things are smart.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If Erin is young then Erin is white.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "white" "+"))
Erin is red.
True
1
proof
[(triple9)]
("Erin" "is" "red" "+")
triple9
Harry is not quiet.
False
1
inv-proof
[(triple11)]
("Harry" "is" "quiet" "-")
triple11
Bob is kind.
True
3
proof
[(((triple4 triple6) -> rule4))]
("Bob" "is" "kind" "+")
((triple4 triple6) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
3
inv-proof
[(((triple4 triple6) -> rule4))]
("Bob" "is" "kind" "-")
((triple4 triple6) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Harry" "is" "smart" "-")
Dave is red.
Unknown
rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Dave" "is" "red" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Bob is furry.[(triple1 OR ((triple2) -> rule2) OR ((triple5) -> rule6))] Bob is quiet.[(triple2)] Bob is red.[(triple3 OR ((((triple4 triple6) -> rule4) triple6) -> rule3))] Bob is smart.[(triple4)] Bob is white.[(triple5)] Bob is young.[(triple6)] Dave is furry.[(triple7)] Erin is furry.[(triple8 OR ((triple10) -> rule6))] Erin is red.[(triple9)] Erin is white.[(triple10)] Harry is quiet.[(triple11)] Harry is young.[(triple12)] @1: Bob is kind.[(((triple4 triple6) -> rule4))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
((triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple5) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
((((triple4 triple6) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
((triple10) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Bob is kind.
("Bob" "is" "kind" "+")
((triple4 triple6) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1