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