Anne is blue. Anne is furry. Anne is not kind. Anne is nice. Anne is red. Anne is round. Charlie is blue. Charlie is not furry. Charlie is kind. Charlie is red. Charlie is round. Dave is blue. Dave is not green. Dave is kind. Dave is red. If Dave is not blue then Dave is furry. If someone is kind and not furry then they are red. If someone is kind and red then they are not nice. If Anne is not red and Anne is not furry then Anne is not nice. If Anne is round then Anne is nice. If someone is nice then they are round.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not kind.
("Anne" "is" "kind" "-")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
If Dave is not blue then Dave is furry.
((("Dave" "is" "blue" "~")) -> ("Dave" "is" "furry" "+"))
If someone is kind and not furry then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "red" "+"))
If someone is kind and red then they are not nice.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "-"))
If Anne is not red and Anne is not furry then Anne is not nice.
((("Anne" "is" "red" "~") ("Anne" "is" "furry" "~")) -> ("Anne" "is" "nice" "-"))
If Anne is round then Anne is nice.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "nice" "+"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Charlie is kind.
True
1
proof
[(triple9)]
("Charlie" "is" "kind" "+")
triple9
Dave is not blue.
False
1
inv-proof
[(triple12)]
("Dave" "is" "blue" "-")
triple12
Dave is not nice.
True
3
proof
[(((triple14 triple15) -> rule3))]
("Dave" "is" "nice" "-")
((triple14 triple15) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Charlie is nice.
False
3
inv-proof
[(((triple9 triple10) -> rule3) OR ((triple9 ((triple9 triple8) -> rule2)) -> rule3))]
("Charlie" "is" "nice" "+")
((triple9 triple10) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
((triple9 ((triple9 triple8) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "round" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Anne is nice.[(triple4 OR ((triple6) -> rule5))] Anne is not kind.[(triple3)] Anne is red.[(triple5)] Anne is round.[(triple6 OR ((triple4) -> rule6))] Charlie is blue.[(triple7)] Charlie is kind.[(triple9)] Charlie is not furry.[(triple8)] Charlie is red.[(triple10 OR ((triple9 triple8) -> rule2))] Charlie is round.[(triple11)] Dave is blue.[(triple12)] Dave is kind.[(triple14)] Dave is not green.[(triple13)] Dave is red.[(triple15)] @1: Charlie is not nice.[(((triple9 triple10) -> rule3) OR ((triple9 ((triple9 triple8) -> rule2)) -> rule3))] Dave is not nice.[(((triple14 triple15) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple6) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple4) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple10
((triple9 triple8) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple11
Dave is blue.
("Dave" "is" "blue" "+")
triple12
Dave is kind.
("Dave" "is" "kind" "+")
triple14
Dave is not green.
("Dave" "is" "green" "-")
triple13
Dave is red.
("Dave" "is" "red" "+")
triple15
Charlie is not nice.
("Charlie" "is" "nice" "-")
((triple9 triple10) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
((triple9 ((triple9 triple8) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
((triple14 triple15) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1