Bob is not cold. Bob is kind. Bob is rough. Bob is smart. Dave is not blue. Dave is red. Dave is smart. Erin is kind. Erin is not red. Erin is rough. If something is rough and not red then it is smart. If something is blue then it is smart. If something is blue then it is furry.
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is rough.
("Erin" "is" "rough" "+")
If something is rough and not red then it is smart.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "smart" "+"))
If something is blue then it is smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is blue then it is furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Erin is rough.
True
1
proof
[(triple10)]
("Erin" "is" "rough" "+")
triple10
Erin is not kind.
False
1
inv-proof
[(triple8)]
("Erin" "is" "kind" "-")
triple8
Erin is smart.
True
3
proof
[(((triple10 triple9) -> rule1))]
("Erin" "is" "smart" "+")
((triple10 triple9) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
3
inv-proof
[(((triple10 triple9) -> rule1))]
("Erin" "is" "smart" "-")
((triple10 triple9) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "furry" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Bob is kind.[(triple2)] Bob is not cold.[(triple1)] Bob is rough.[(triple3)] Bob is smart.[(triple4)] Dave is not blue.[(triple5)] Dave is red.[(triple6)] Dave is smart.[(triple7)] Erin is kind.[(triple8)] Erin is not red.[(triple9)] Erin is rough.[(triple10)] @1: Erin is smart.[(((triple10 triple9) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is not cold.
("Bob" "is" "cold" "-")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Dave is not blue.
("Dave" "is" "blue" "-")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is not red.
("Erin" "is" "red" "-")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
((triple10 triple9) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1