Anne is rough. Bob is furry. Bob is rough. Bob is white. Dave is big. Dave is furry. Dave is rough. Dave is smart. Dave is white. Erin is furry. Erin is round. Erin is white. Round people are rough. If someone is furry and blue then they are rough. Furry people are blue. Furry, big people are blue. Furry people are blue. All blue people are white. Blue people are furry. Big people are round.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry and blue then they are rough.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Furry, big people are blue.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
All blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Dave is not smart.
False
1
inv-proof
[(triple8)]
("Dave" "is" "smart" "-")
triple8
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "round" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is rough.[(triple1)] Bob is furry.[(triple2)] Bob is rough.[(triple3 OR ((triple2 ((triple2) -> rule3)) -> rule2) OR ((triple2 ((triple2) -> rule5)) -> rule2))] Bob is white.[(triple4 OR ((((triple2) -> rule3)) -> rule6) OR ((((triple2) -> rule5)) -> rule6))] Dave is big.[(triple5)] Dave is furry.[(triple6)] Dave is rough.[(triple7 OR ((((triple5) -> rule8)) -> rule1) OR ((triple6 ((triple6) -> rule3)) -> rule2) OR ((triple6 ((triple6) -> rule5)) -> rule2) OR ((triple6 ((triple6 triple5) -> rule4)) -> rule2))] Dave is smart.[(triple8)] Dave is white.[(triple9 OR ((((triple6) -> rule3)) -> rule6) OR ((((triple6) -> rule5)) -> rule6) OR ((((triple6 triple5) -> rule4)) -> rule6))] Erin is furry.[(triple10)] Erin is round.[(triple11)] Erin is white.[(triple12 OR ((((triple10) -> rule3)) -> rule6) OR ((((triple10) -> rule5)) -> rule6))] @1: Bob is blue.[(((triple2) -> rule3) OR ((triple2) -> rule5))] Dave is blue.[(((triple6) -> rule3) OR ((triple6) -> rule5) OR ((triple6 triple5) -> rule4))] Dave is round.[(((triple5) -> rule8))] Erin is blue.[(((triple10) -> rule3) OR ((triple10) -> rule5))] Erin is rough.[(((triple11) -> rule1) OR ((triple10 ((triple10) -> rule3)) -> rule2) OR ((triple10 ((triple10) -> rule5)) -> rule2))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple2 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple4
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
((((triple5) -> (rule8 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple6 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((triple6 ((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((triple6 ((triple6 triple5) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple8
Dave is white.
("Dave" "is" "white" "+")
triple9
((((triple6) -> (rule3 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple6 triple5) -> (rule4 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
triple12
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple2) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple6) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6 triple5) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple5) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple10) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple10) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple11) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple10 ((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((triple10 ((triple10) -> (rule5 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2