Anne is blue. Anne is green. Anne is kind. Anne is quiet. Anne is red. Anne is round. Anne is young. If Anne is kind then Anne is quiet. If Anne is quiet then Anne is round. All young, green people are red.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
If Anne is kind then Anne is quiet.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "quiet" "+"))
If Anne is quiet then Anne is round.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "round" "+"))
All young, green people are red.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Anne is red.
True
1
proof
[(triple5 OR ((triple7 triple2) -> rule3))]
("Anne" "is" "red" "+")
triple5
((triple7 triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not quiet.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule1))]
("Anne" "is" "quiet" "-")
triple4
((triple3) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is kind.[(triple3)] Anne is quiet.[(triple4 OR ((triple3) -> rule1))] Anne is red.[(triple5 OR ((triple7 triple2) -> rule3))] Anne is round.[(triple6 OR ((triple4) -> rule2) OR ((((triple3) -> rule1)) -> rule2))] Anne is young.[(triple7)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple3) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple5
((triple7 triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple4) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple7