Anne is blue. Anne is furry. Anne is red. Anne is round. Gary is furry. Gary is red. Gary is white. If someone is furry and red then they are round. All furry, round people are red. If someone is furry then they are red. All smart, white people are kind. If Anne is smart and Anne is furry then Anne is round. All round, red people are furry. Furry, smart people are blue. Round people are kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is furry and red then they are round.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
All furry, round people are red.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is furry then they are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All smart, white people are kind.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If Anne is smart and Anne is furry then Anne is round.
((("Anne" "is" "smart" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "round" "+"))
All round, red people are furry.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Furry, smart people are blue.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Anne is furry.
True
1
proof
[(triple2 OR ((triple4 triple3) -> rule6))]
("Anne" "is" "furry" "+")
triple2
((triple4 triple3) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
1
inv-proof
[(triple2 OR ((triple4 triple3) -> rule6))]
("Anne" "is" "furry" "-")
triple2
((triple4 triple3) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Gary is round.
True
3
proof
[(((triple5 triple6) -> rule1) OR ((triple5 ((triple5) -> rule3)) -> rule1))]
("Gary" "is" "round" "+")
((triple5 triple6) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Anne is not kind.
False
2
inv-proof
[(((triple4) -> rule8) OR ((((triple2 triple3) -> rule1)) -> rule8) OR ((((triple2 ((triple2) -> rule3)) -> rule1)) -> rule8))]
("Anne" "is" "kind" "-")
((triple4) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple2 triple3) -> (rule1 % int2))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "blue" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2 OR ((triple4 triple3) -> rule6))] Anne is red.[(triple3 OR ((triple2) -> rule3) OR ((triple2 triple4) -> rule2))] Anne is round.[(triple4 OR ((triple2 triple3) -> rule1) OR ((triple2 ((triple2) -> rule3)) -> rule1))] Gary is furry.[(triple5)] Gary is red.[(triple6 OR ((triple5) -> rule3))] Gary is white.[(triple7)] @1: Anne is kind.[(((triple4) -> rule8) OR ((((triple2 triple3) -> rule1)) -> rule8) OR ((((triple2 ((triple2) -> rule3)) -> rule1)) -> rule8))] Gary is round.[(((triple5 triple6) -> rule1) OR ((triple5 ((triple5) -> rule3)) -> rule1))] @2: Gary is kind.[(((((triple5 triple6) -> rule1)) -> rule8) OR ((((triple5 ((triple5) -> rule3)) -> rule1)) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple4 triple3) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 triple4) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple4
((triple2 triple3) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple2 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
((triple5) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple7
Anne is kind.
("Anne" "is" "kind" "+")
((triple4) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple2 triple3) -> (rule1 % int2))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
((triple5 triple6) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple5 triple6) -> (rule1 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple5 ((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3