Anne is big. Anne is blue. Anne is cold. Anne is furry. Anne is kind. Gary is big. Gary is blue. Gary is cold. Gary is furry. Gary is kind. Gary is red. Gary is smart. If something is smart then it is cold. Furry things are cold. If something is smart and not big then it is cold. If something is kind then it is cold. All cold, red things are kind. If something is smart and not big then it is kind.
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 kind.
("Anne" "is" "kind" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is smart then it is cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is smart and not big then it is cold.
((("something" "is" "smart" "+") ("something" "is" "big" "~")) -> ("something" "is" "cold" "+"))
If something is kind then it is cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
All cold, red things are kind.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is smart and not big then it is kind.
((("something" "is" "smart" "+") ("something" "is" "big" "~")) -> ("something" "is" "kind" "+"))
Gary is smart.
True
1
proof
[(triple12)]
("Gary" "is" "smart" "+")
triple12
Anne is not blue.
False
1
inv-proof
[(triple2)]
("Anne" "is" "blue" "-")
triple2
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is cold.[(triple3 OR ((triple4) -> rule2) OR ((triple5) -> rule4))] Anne is furry.[(triple4)] Anne is kind.[(triple5)] Gary is big.[(triple6)] Gary is blue.[(triple7)] Gary is cold.[(triple8 OR ((triple10) -> rule4) OR ((triple12) -> rule1) OR ((triple9) -> rule2))] Gary is furry.[(triple9)] Gary is kind.[(triple10 OR ((triple8 triple11) -> rule5) OR ((((triple12) -> rule1) triple11) -> rule5) OR ((((triple9) -> rule2) triple11) -> rule5))] Gary is red.[(triple11)] Gary is smart.[(triple12)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
((triple4) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple5) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
((triple10) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple12) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple9) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
((triple8 triple11) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple12) -> (rule1 % int2)) triple11) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple9) -> (rule2 % int2)) triple11) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12