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