Anne is big. Anne is blue. Anne is cold. Anne is furry. Anne is kind. Anne is quiet. Anne is not smart. If something is furry then it is quiet. If something is kind and smart then it is cold. If Anne is quiet then Anne is cold.
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" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is kind and smart then it is cold.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If Anne is quiet then Anne is cold.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "cold" "+"))
Anne is cold.
True
1
proof
[(triple3 OR ((triple6) -> rule3) OR ((((triple4) -> rule1)) -> rule3))]
("Anne" "is" "cold" "+")
triple3
((triple6) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not cold.
False
1
inv-proof
[(triple3 OR ((triple6) -> rule3) OR ((((triple4) -> rule1)) -> rule3))]
("Anne" "is" "cold" "-")
triple3
((triple6) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is cold.[(triple3 OR ((triple6) -> rule3) OR ((((triple4) -> rule1)) -> rule3))] Anne is furry.[(triple4)] Anne is kind.[(triple5)] Anne is not smart.[(triple7)] Anne is quiet.[(triple6 OR ((triple4) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
((triple6) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
triple5
Anne is not smart.
("Anne" "is" "smart" "-")
triple7
Anne is quiet.
("Anne" "is" "quiet" "+")
triple6
((triple4) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1