Anne is cold. Anne is red. Anne is round. If someone is white then they are blue. All cold, blue people are big. All cold, big people are blue. If someone is young and big then they are red. If someone is cold and round then they are white. If someone is big and blue then they are white.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
If someone is white then they are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
All cold, blue people are big.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
All cold, big people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone is young and big then they are red.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is cold and round then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If someone is big and blue then they are white.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Anne is not round.
False
1
inv-proof
[(triple3)]
("Anne" "is" "round" "-")
triple3
Anne is white.
True
3
proof
[(((triple1 triple3) -> rule5))]
("Anne" "is" "white" "+")
((triple1 triple3) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
3
inv-proof
[(((triple1 triple3) -> rule5))]
("Anne" "is" "white" "-")
((triple1 triple3) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
True
4
proof
[(((((triple1 triple3) -> rule5)) -> rule1))]
("Anne" "is" "blue" "+")
((((triple1 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not blue.
False
4
inv-proof
[(((((triple1 triple3) -> rule5)) -> rule1))]
("Anne" "is" "blue" "-")
((((triple1 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is big.
True
6
proof
[(((triple1 ((((triple1 triple3) -> rule5)) -> rule1)) -> rule2))]
("Anne" "is" "big" "+")
((triple1 ((((triple1 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not big.
False
6
inv-proof
[(((triple1 ((((triple1 triple3) -> rule5)) -> rule1)) -> rule2))]
("Anne" "is" "big" "-")
((triple1 ((((triple1 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
@0: Anne is cold.[(triple1)] Anne is red.[(triple2)] Anne is round.[(triple3)] @1: Anne is white.[(((triple1 triple3) -> rule5))] @2: Anne is blue.[(((((triple1 triple3) -> rule5)) -> rule1))] @3: Anne is big.[(((triple1 ((((triple1 triple3) -> rule5)) -> rule1)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
((triple1 triple3) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((triple1 ((((triple1 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3