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