Anne is green. Anne is red. Anne is young. All young, red things are round. All red things are round. All red things are blue. Red things are blue. If something is cold and young then it is green. If Anne is cold and Anne is red then Anne is green. If something is nice and not round then it is not cold. If something is green and young then it is cold.
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
All young, red things are round.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
All red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something is cold and young then it is green.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If Anne is cold and Anne is red then Anne is green.
((("Anne" "is" "cold" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "green" "+"))
If something is nice and not round then it is not cold.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "is" "cold" "-"))
If something is green and young then it is cold.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
Anne is red.
True
1
proof
[(triple2)]
("Anne" "is" "red" "+")
triple2
Anne is not red.
False
1
inv-proof
[(triple2)]
("Anne" "is" "red" "-")
triple2
Anne is round.
True
2
proof
[(((triple2) -> rule2) OR ((triple3 triple2) -> rule1))]
("Anne" "is" "round" "+")
((triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3 triple2) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple2) -> rule3) OR ((triple2) -> rule4))]
("Anne" "is" "blue" "-")
((triple2) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple2) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
@0: Anne is green.[(triple1)] Anne is red.[(triple2)] Anne is young.[(triple3)] @1: Anne is blue.[(((triple2) -> rule3) OR ((triple2) -> rule4))] Anne is cold.[(((triple1 triple3) -> rule8))] Anne is round.[(((triple2) -> rule2) OR ((triple3 triple2) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple2) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 triple3) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3 triple2) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1