Anne is blue. Anne is furry. Anne is kind. Anne is nice. Bob is big. Bob is blue. Bob is furry. Bob is kind. Bob is nice. Bob is quiet. Bob is smart. Gary is big. Gary is furry. Gary is nice. Gary is quiet. Gary is smart. All big things are blue. If something is blue and nice then it is kind. Blue, furry things are smart. All nice things are furry. All smart things are nice. All quiet, kind things are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is blue and nice then it is kind.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Blue, furry things are smart.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
All nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All quiet, kind things are blue.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Gary is furry.
True
1
proof
[(triple13 OR ((triple14) -> rule4) OR ((((triple16) -> rule5)) -> rule4))]
("Gary" "is" "furry" "+")
triple13
((triple14) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple16) -> (rule5 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Bob is not furry.
False
1
inv-proof
[(triple7 OR ((triple9) -> rule4) OR ((((triple11) -> rule5)) -> rule4))]
("Bob" "is" "furry" "-")
triple7
((triple9) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple11) -> (rule5 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Gary is blue.
True
2
proof
[(((triple12) -> rule1))]
("Gary" "is" "blue" "+")
((triple12) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple12) -> rule1))]
("Gary" "is" "blue" "-")
((triple12) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
True
4
proof
[(((((triple12) -> rule1) triple14) -> rule2) OR ((((triple12) -> rule1) ((triple16) -> rule5)) -> rule2) OR ((((triple12) -> rule1) ((((((triple12) -> rule1) triple13) -> rule3)) -> rule5)) -> rule2))]
("Gary" "is" "kind" "+")
((((triple12) -> (rule1 % int2)) triple14) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple12) -> (rule1 % int3)) ((triple16) -> (rule5 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((triple12) -> (rule1 % int4)) ((((((triple12) -> (rule1 % int4)) triple13) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is not kind.
False
4
inv-proof
[(((((triple12) -> rule1) triple14) -> rule2) OR ((((triple12) -> rule1) ((triple16) -> rule5)) -> rule2) OR ((((triple12) -> rule1) ((((((triple12) -> rule1) triple13) -> rule3)) -> rule5)) -> rule2))]
("Gary" "is" "kind" "-")
((((triple12) -> (rule1 % int2)) triple14) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple12) -> (rule1 % int3)) ((triple16) -> (rule5 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((triple12) -> (rule1 % int4)) ((((((triple12) -> (rule1 % int4)) triple13) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2 OR ((triple4) -> rule4))] Anne is kind.[(triple3 OR ((triple1 triple4) -> rule2) OR ((triple1 ((((triple1 triple2) -> rule3)) -> rule5)) -> rule2))] Anne is nice.[(triple4 OR ((((triple1 triple2) -> rule3)) -> rule5))] Bob is big.[(triple5)] Bob is blue.[(triple6 OR ((triple5) -> rule1) OR ((triple10 triple8) -> rule6))] Bob is furry.[(triple7 OR ((triple9) -> rule4) OR ((((triple11) -> rule5)) -> rule4))] Bob is kind.[(triple8 OR ((triple6 triple9) -> rule2) OR ((triple6 ((triple11) -> rule5)) -> rule2) OR ((((triple5) -> rule1) triple9) -> rule2) OR ((((triple5) -> rule1) ((triple11) -> rule5)) -> rule2) OR ((triple6 ((((triple6 triple7) -> rule3)) -> rule5)) -> rule2) OR ((((triple5) -> rule1) ((((triple6 triple7) -> rule3)) -> rule5)) -> rule2) OR ((triple6 ((((((triple5) -> rule1) triple7) -> rule3)) -> rule5)) -> rule2) OR ((((triple5) -> rule1) ((((((triple5) -> rule1) triple7) -> rule3)) -> rule5)) -> rule2))] Bob is nice.[(triple9 OR ((triple11) -> rule5) OR ((((triple6 triple7) -> rule3)) -> rule5) OR ((((((triple5) -> rule1) triple7) -> rule3)) -> rule5) OR ((((((triple10 triple8) -> rule6) triple7) -> rule3)) -> rule5))] Bob is quiet.[(triple10)] Bob is smart.[(triple11 OR ((triple6 triple7) -> rule3) OR ((triple6 ((triple9) -> rule4)) -> rule3) OR ((((triple5) -> rule1) triple7) -> rule3) OR ((((triple10 triple8) -> rule6) triple7) -> rule3) OR ((((triple5) -> rule1) ((triple9) -> rule4)) -> rule3) OR ((((triple10 triple8) -> rule6) ((triple9) -> rule4)) -> rule3))] Gary is big.[(triple12)] Gary is furry.[(triple13 OR ((triple14) -> rule4) OR ((((triple16) -> rule5)) -> rule4))] Gary is nice.[(triple14 OR ((triple16) -> rule5) OR ((((((triple12) -> rule1) triple13) -> rule3)) -> rule5))] Gary is quiet.[(triple15)] Gary is smart.[(triple16 OR ((((triple12) -> rule1) triple13) -> rule3) OR ((((triple12) -> rule1) ((triple14) -> rule4)) -> rule3))] @1: Anne is smart.[(((triple1 triple2) -> rule3) OR ((triple1 ((triple4) -> rule4)) -> rule3))] Gary is blue.[(((triple12) -> rule1))] @2: Gary is kind.[(((((triple12) -> rule1) triple14) -> rule2) OR ((((triple12) -> rule1) ((triple16) -> rule5)) -> rule2) OR ((((triple12) -> rule1) ((((((triple12) -> rule1) triple13) -> rule3)) -> rule5)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple4) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple1 triple4) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1 ((((triple1 triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((((triple1 triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
triple5
Bob is blue.
("Bob" "is" "blue" "+")
triple6
((triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple10 triple8) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple7
((triple9) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple11) -> (rule5 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple8
((triple6 triple9) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple6 ((triple11) -> (rule5 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple5) -> (rule1 % int2)) triple9) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple11) -> (rule5 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((triple6 ((((triple6 triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((triple5) -> (rule1 % int4)) ((((triple6 triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
((triple6 ((((((triple5) -> (rule1 % int4)) triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
((((triple5) -> (rule1 % int4)) ((((((triple5) -> (rule1 % int4)) triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
triple9
((triple11) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple6 triple7) -> (rule3 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((triple5) -> (rule1 % int3)) triple7) -> (rule3 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((triple10 triple8) -> (rule6 % int3)) triple7) -> (rule3 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple10
Bob is smart.
("Bob" "is" "smart" "+")
triple11
((triple6 triple7) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple6 ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple5) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple10 triple8) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((triple10 triple8) -> (rule6 % int3)) ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
triple12
Gary is furry.
("Gary" "is" "furry" "+")
triple13
((triple14) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple16) -> (rule5 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple14
((triple16) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((((triple12) -> (rule1 % int3)) triple13) -> (rule3 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple15
Gary is smart.
("Gary" "is" "smart" "+")
triple16
((((triple12) -> (rule1 % int2)) triple13) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple12) -> (rule1 % int3)) ((triple14) -> (rule4 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple12) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple12) -> (rule1 % int2)) triple14) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple12) -> (rule1 % int3)) ((triple16) -> (rule5 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((triple12) -> (rule1 % int4)) ((((((triple12) -> (rule1 % int4)) triple13) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4