Anne is blue. Anne is nice. Anne is not young. Harry is blue. Harry is nice. Harry is smart. Harry is young. If Anne is furry and Anne is not nice then Anne is quiet. If something is blue then it is cold. If something is cold and not blue then it is smart. If something is cold and not blue then it is smart. All nice things are furry. If Anne is furry then Anne is smart. If something is cold and not smart then it is not quiet. If something is blue then it is quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not young.
("Anne" "is" "young" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If Anne is furry and Anne is not nice then Anne is quiet.
((("Anne" "is" "furry" "+") ("Anne" "is" "nice" "~")) -> ("Anne" "is" "quiet" "+"))
If something is blue then it is cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is cold and not blue then it is smart.
((("something" "is" "cold" "+") ("something" "is" "blue" "~")) -> ("something" "is" "smart" "+"))
If something is cold and not blue then it is smart.
((("something" "is" "cold" "+") ("something" "is" "blue" "~")) -> ("something" "is" "smart" "+"))
All nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If Anne is furry then Anne is smart.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "smart" "+"))
If something is cold and not smart then it is not quiet.
((("something" "is" "cold" "+") ("something" "is" "smart" "~")) -> ("something" "is" "quiet" "-"))
If something is blue then it is quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Harry is young.
True
1
proof
[(triple7)]
("Harry" "is" "young" "+")
triple7
Anne is not nice.
False
1
inv-proof
[(triple2)]
("Anne" "is" "nice" "-")
triple2
Harry is cold.
True
2
proof
[(((triple4) -> rule2))]
("Harry" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple2) -> rule5))]
("Anne" "is" "furry" "-")
((triple2) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2)] Anne is not young.[(triple3)] Harry is blue.[(triple4)] Harry is nice.[(triple5)] Harry is smart.[(triple6)] Harry is young.[(triple7)] @1: Anne is cold.[(((triple1) -> rule2))] Anne is furry.[(((triple2) -> rule5))] Anne is quiet.[(((triple1) -> rule8))] Harry is cold.[(((triple4) -> rule2))] Harry is furry.[(((triple5) -> rule5))] Harry is quiet.[(((triple4) -> rule8))] @2: Anne is smart.[(((((triple2) -> rule5)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is not young.
("Anne" "is" "young" "-")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple5
Harry is smart.
("Harry" "is" "smart" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple5) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2