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