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