Anne is big. Anne is blue. Anne is cold. Anne is furry. Anne is nice. Anne is not red. Anne is round. Furry things are cold. Red, cold things are not round. If Anne is red and Anne is round then Anne is not blue. Blue things are nice. If something is red and not cold then it is blue. Furry, round things are blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is round.
("Anne" "is" "round" "+")
Furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Red, cold things are not round.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "-"))
If Anne is red and Anne is round then Anne is not blue.
((("Anne" "is" "red" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "blue" "-"))
Blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is red and not cold then it is blue.
((("something" "is" "red" "+") ("something" "is" "cold" "~")) -> ("something" "is" "blue" "+"))
Furry, round things are blue.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Anne is round.
True
1
proof
[(triple7)]
("Anne" "is" "round" "+")
triple7
Anne is not blue.
False
1
inv-proof
[(triple2 OR ((triple4 triple7) -> rule6))]
("Anne" "is" "blue" "-")
triple2
((triple4 triple7) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple4 triple7) -> rule6))] Anne is cold.[(triple3 OR ((triple4) -> rule1))] Anne is furry.[(triple4)] Anne is nice.[(triple5 OR ((triple2) -> rule4) OR ((((triple4 triple7) -> rule6)) -> rule4))] Anne is not red.[(triple6)] Anne is round.[(triple7)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple4 triple7) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
triple3
((triple4) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
triple5
((triple2) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple4 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not red.
("Anne" "is" "red" "-")
triple6
Anne is round.
("Anne" "is" "round" "+")
triple7