Anne is blue. Anne is furry. Anne is kind. All furry, red people are round. If someone is green and blue then they are rough. All red, rough people are blue. If Anne is blue and Anne is round then Anne is rough. All rough people are red. If someone is blue and furry then they are red.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
All furry, red people are round.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is green and blue then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
All red, rough people are blue.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If Anne is blue and Anne is round then Anne is rough.
((("Anne" "is" "blue" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "rough" "+"))
All rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and furry then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Anne is not kind.
False
1
inv-proof
[(triple3)]
("Anne" "is" "kind" "-")
triple3
Anne is red.
True
3
proof
[(((triple1 triple2) -> rule6))]
("Anne" "is" "red" "+")
((triple1 triple2) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not red.
False
3
inv-proof
[(((triple1 triple2) -> rule6))]
("Anne" "is" "red" "-")
((triple1 triple2) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
True
5
proof
[(((triple2 ((triple1 triple2) -> rule6)) -> rule1))]
("Anne" "is" "round" "+")
((triple2 ((triple1 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not round.
False
5
inv-proof
[(((triple2 ((triple1 triple2) -> rule6)) -> rule1))]
("Anne" "is" "round" "-")
((triple2 ((triple1 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
True
7
proof
[(((triple1 ((triple2 ((triple1 triple2) -> rule6)) -> rule1)) -> rule4))]
("Anne" "is" "rough" "+")
((triple1 ((triple2 ((triple1 triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is not rough.
False
7
inv-proof
[(((triple1 ((triple2 ((triple1 triple2) -> rule6)) -> rule1)) -> rule4))]
("Anne" "is" "rough" "-")
((triple1 ((triple2 ((triple1 triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Anne is kind.[(triple3)] @1: Anne is red.[(((triple1 triple2) -> rule6))] @2: Anne is round.[(((triple2 ((triple1 triple2) -> rule6)) -> rule1))] @3: Anne is rough.[(((triple1 ((triple2 ((triple1 triple2) -> rule6)) -> rule1)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
((triple1 triple2) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple2 ((triple1 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 ((triple2 ((triple1 triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3