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