Anne is big. Anne is cold. Anne is furry. Anne is kind. Anne is nice. Anne is red. Anne is white. Charlie is big. Charlie is cold. Charlie is furry. Charlie is kind. Charlie is white. Cold things are furry. White things are nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
White things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Anne is kind.
True
1
proof
[(triple4)]
("Anne" "is" "kind" "+")
triple4
Charlie is not furry.
False
1
inv-proof
[(triple10 OR ((triple9) -> rule1))]
("Charlie" "is" "furry" "-")
triple10
((triple9) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is furry.[(triple3 OR ((triple2) -> rule1))] Anne is kind.[(triple4)] Anne is nice.[(triple5 OR ((triple7) -> rule2))] Anne is red.[(triple6)] Anne is white.[(triple7)] Charlie is big.[(triple8)] Charlie is cold.[(triple9)] Charlie is furry.[(triple10 OR ((triple9) -> rule1))] Charlie is kind.[(triple11)] Charlie is white.[(triple12)] @1: Charlie is nice.[(((triple12) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple2) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
triple5
((triple7) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple6
Anne is white.
("Anne" "is" "white" "+")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
triple8
Charlie is cold.
("Charlie" "is" "cold" "+")
triple9
Charlie is furry.
("Charlie" "is" "furry" "+")
triple10
((triple9) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple11
Charlie is white.
("Charlie" "is" "white" "+")
triple12
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple12) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1