Anne is furry. Anne is smart. Charlie is nice. Charlie is smart. Harry is big. Harry is red. Harry is white. If Anne is big and Anne is round then Anne is smart. If Charlie is big then Charlie is red. If someone is red then they are furry. If someone is round and nice then they are red. If someone is white and furry then they are nice. If someone is white then they are furry.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
If Anne is big and Anne is round then Anne is smart.
((("Anne" "is" "big" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "smart" "+"))
If Charlie is big then Charlie is red.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "red" "+"))
If someone is red then they are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If someone is round and nice then they are red.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is white and furry then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is white then they are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Harry is white.
True
1
proof
[(triple7)]
("Harry" "is" "white" "+")
triple7
Charlie is not smart.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "smart" "-")
triple4
Harry is furry.
True
2
proof
[(((triple6) -> rule3) OR ((triple7) -> rule6))]
("Harry" "is" "furry" "+")
((triple6) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple7) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple6) -> rule3) OR ((triple7) -> rule6))]
("Harry" "is" "furry" "-")
((triple6) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple7) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
True
4
proof
[(((triple7 ((triple6) -> rule3)) -> rule5) OR ((triple7 ((triple7) -> rule6)) -> rule5))]
("Harry" "is" "nice" "+")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple7 ((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not nice.
False
4
inv-proof
[(((triple7 ((triple6) -> rule3)) -> rule5) OR ((triple7 ((triple7) -> rule6)) -> rule5))]
("Harry" "is" "nice" "-")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple7 ((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "nice" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not furry.
Unknown
inv-rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "furry" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is furry.[(triple1)] Anne is smart.[(triple2)] Charlie is nice.[(triple3)] Charlie is smart.[(triple4)] Harry is big.[(triple5)] Harry is red.[(triple6)] Harry is white.[(triple7)] @1: Harry is furry.[(((triple6) -> rule3) OR ((triple7) -> rule6))] @2: Harry is nice.[(((triple7 ((triple6) -> rule3)) -> rule5) OR ((triple7 ((triple7) -> rule6)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
((triple6) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple7) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple7 ((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2