Anne is blue. Anne is kind. Anne is nice. Anne is quiet. Anne is red. Anne is smart. Anne is young. If Anne is quiet and Anne is nice then Anne is red. All kind things are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
If Anne is quiet and Anne is nice then Anne is red.
((("Anne" "is" "quiet" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "red" "+"))
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Anne is blue.
True
1
proof
[(triple1 OR ((triple2) -> rule2))]
("Anne" "is" "blue" "+")
triple1
((triple2) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not smart.
False
1
inv-proof
[(triple6)]
("Anne" "is" "smart" "-")
triple6
@0: Anne is blue.[(triple1 OR ((triple2) -> rule2))] Anne is kind.[(triple2)] Anne is nice.[(triple3)] Anne is quiet.[(triple4)] Anne is red.[(triple5 OR ((triple4 triple3) -> rule1))] Anne is smart.[(triple6)] Anne is young.[(triple7)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple2) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple5
((triple4 triple3) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7