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