Anne is big. Anne is blue. Anne is kind. Anne is quiet. Anne is red. Anne is not smart. Bob is big. Bob is blue. Bob is kind. Bob is quiet. Bob is red. Bob is not smart. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is smart. If something is kind then it is not furry. If something is smart and quiet then it is big. If something is red and not furry then it is blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If something is kind then it is not furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "-"))
If something is smart and quiet then it is big.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is red and not furry then it is blue.
((("something" "is" "red" "+") ("something" "is" "furry" "~")) -> ("something" "is" "blue" "+"))
Bob is red.
True
1
proof
[(triple11)]
("Bob" "is" "red" "+")
triple11
Anne is not red.
False
1
inv-proof
[(triple5)]
("Anne" "is" "red" "-")
triple5
Charlie is not furry.
True
2
proof
[(((triple13) -> rule1))]
("Charlie" "is" "furry" "-")
((triple13) -> (rule1 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Anne is furry.
False
2
inv-proof
[(((triple3) -> rule1))]
("Anne" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Charlie is blue.
True
4
proof
[(((triple15 ((triple13) -> rule1)) -> rule3))]
("Charlie" "is" "blue" "+")
((triple15 ((triple13) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
int2
Charlie is not blue.
False
4
inv-proof
[(((triple15 ((triple13) -> rule1)) -> rule3))]
("Charlie" "is" "blue" "-")
((triple15 ((triple13) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
int2
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple5 ((triple3) -> rule1)) -> rule3))] Anne is kind.[(triple3)] Anne is not smart.[(triple6)] Anne is quiet.[(triple4)] Anne is red.[(triple5)] Bob is big.[(triple7)] Bob is blue.[(triple8 OR ((triple11 ((triple9) -> rule1)) -> rule3))] Bob is kind.[(triple9)] Bob is not smart.[(triple12)] Bob is quiet.[(triple10)] Bob is red.[(triple11)] Charlie is kind.[(triple13)] Charlie is quiet.[(triple14)] Charlie is red.[(triple15)] Charlie is smart.[(triple16)] @1: Anne is not furry.[(((triple3) -> rule1))] Bob is not furry.[(((triple9) -> rule1))] Charlie is big.[(((triple16 triple14) -> rule2))] Charlie is not furry.[(((triple13) -> rule1))] @2: Charlie is blue.[(((triple15 ((triple13) -> rule1)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple5 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not furry.
("Anne" "is" "furry" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is not smart.
("Anne" "is" "smart" "-")
triple6
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple5
Bob is big.
("Bob" "is" "big" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
triple8
((triple11 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple9
Bob is not smart.
("Bob" "is" "smart" "-")
triple12
Bob is quiet.
("Bob" "is" "quiet" "+")
triple10
Bob is red.
("Bob" "is" "red" "+")
triple11
Charlie is kind.
("Charlie" "is" "kind" "+")
triple13
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple14
Charlie is red.
("Charlie" "is" "red" "+")
triple15
Charlie is smart.
("Charlie" "is" "smart" "+")
triple16
Anne is not furry.
("Anne" "is" "furry" "-")
((triple3) -> (rule1 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
((triple9) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple16 triple14) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
((triple13) -> (rule1 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple15 ((triple13) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
int2