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