Anne is furry. Anne is green. Anne is red. Anne is rough. Anne is smart. Anne is young. Bob is green. Bob is quiet. Bob is red. Bob is rough. Bob is smart. Bob is young. Erin is green. Erin is young. Gary is smart. Gary is young. Quiet things are furry. If something is green and smart then it is rough. If something is young and smart then it is furry. All green things are red. All rough, quiet things are red. All red, green things are quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is green and smart then it is rough.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is young and smart then it is furry.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All rough, quiet things are red.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
All red, green things are quiet.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Anne is smart.
True
1
proof
[(triple5)]
("Anne" "is" "smart" "+")
triple5
Anne is not furry.
False
1
inv-proof
[(triple1 OR ((triple6 triple5) -> rule3) OR ((((triple3 triple2) -> rule6)) -> rule1) OR ((((((triple2) -> rule4) triple2) -> rule6)) -> rule1))]
("Anne" "is" "furry" "-")
triple1
((triple6 triple5) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple3 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((((triple2) -> (rule4 % int3)) triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Erin is red.
True
2
proof
[(((triple13) -> rule4))]
("Erin" "is" "red" "+")
((triple13) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple8) -> rule1) OR ((triple12 triple11) -> rule3) OR ((((triple9 triple7) -> rule6)) -> rule1) OR ((((((triple7) -> rule4) triple7) -> rule6)) -> rule1))]
("Bob" "is" "furry" "-")
((triple8) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple12 triple11) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple9 triple7) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple7) -> (rule4 % int3)) triple7) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Erin is quiet.
True
4
proof
[(((((triple13) -> rule4) triple13) -> rule6))]
("Erin" "is" "quiet" "+")
((((triple13) -> (rule4 % int2)) triple13) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not quiet.
False
4
inv-proof
[(((((triple13) -> rule4) triple13) -> rule6))]
("Erin" "is" "quiet" "-")
((((triple13) -> (rule4 % int2)) triple13) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "rough" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not red.
Unknown
inv-rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Anne is furry.[(triple1 OR ((triple6 triple5) -> rule3) OR ((((triple3 triple2) -> rule6)) -> rule1) OR ((((((triple2) -> rule4) triple2) -> rule6)) -> rule1))] Anne is green.[(triple2)] Anne is red.[(triple3 OR ((triple2) -> rule4))] Anne is rough.[(triple4 OR ((triple2 triple5) -> rule2))] Anne is smart.[(triple5)] Anne is young.[(triple6)] Bob is green.[(triple7)] Bob is quiet.[(triple8 OR ((triple9 triple7) -> rule6) OR ((((triple7) -> rule4) triple7) -> rule6))] Bob is red.[(triple9 OR ((triple7) -> rule4) OR ((triple10 triple8) -> rule5) OR ((((triple7 triple11) -> rule2) triple8) -> rule5))] Bob is rough.[(triple10 OR ((triple7 triple11) -> rule2))] Bob is smart.[(triple11)] Bob is young.[(triple12)] Erin is green.[(triple13)] Erin is young.[(triple14)] Gary is smart.[(triple15)] Gary is young.[(triple16)] @1: Anne is quiet.[(((triple3 triple2) -> rule6) OR ((((triple2) -> rule4) triple2) -> rule6))] Bob is furry.[(((triple8) -> rule1) OR ((triple12 triple11) -> rule3) OR ((((triple9 triple7) -> rule6)) -> rule1) OR ((((((triple7) -> rule4) triple7) -> rule6)) -> rule1))] Erin is red.[(((triple13) -> rule4))] Gary is furry.[(((triple16 triple15) -> rule3))] @2: Erin is quiet.[(((((triple13) -> rule4) triple13) -> rule6))] @3: Erin is furry.[(((((((triple13) -> rule4) triple13) -> rule6)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple6 triple5) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple3 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((((triple2) -> (rule4 % int3)) triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple2) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple2 triple5) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is young.
("Anne" "is" "young" "+")
triple6
Bob is green.
("Bob" "is" "green" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
triple8
((triple9 triple7) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple7) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple9
((triple7) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple10 triple8) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple7 triple11) -> (rule2 % int2)) triple8) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple10
((triple7 triple11) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple11
Bob is young.
("Bob" "is" "young" "+")
triple12
Erin is green.
("Erin" "is" "green" "+")
triple13
Erin is young.
("Erin" "is" "young" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple3 triple2) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple2) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((triple8) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple12 triple11) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple9 triple7) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple7) -> (rule4 % int3)) triple7) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((triple13) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple16 triple15) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple13) -> (rule4 % int2)) triple13) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((((triple13) -> (rule4 % int3)) triple13) -> (rule6 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3