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