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