Bob is blue. Bob is furry. Bob is green. Bob is not kind. Bob is nice. Bob is red. Bob is smart. Fiona is blue. Fiona is furry. Fiona is not green. Fiona is kind. Fiona is nice. Fiona is red. Fiona is smart. If someone is kind then they are nice. All kind, furry people are blue. Nice people are furry.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is not green.
("Fiona" "is" "green" "-")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All kind, furry people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Bob is smart.
True
1
proof
[(triple7)]
("Bob" "is" "smart" "+")
triple7
Fiona is not kind.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "kind" "-")
triple11
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2 OR ((triple5) -> rule3))] Bob is green.[(triple3)] Bob is nice.[(triple5)] Bob is not kind.[(triple4)] Bob is red.[(triple6)] Bob is smart.[(triple7)] Fiona is blue.[(triple8 OR ((triple11 triple9) -> rule2) OR ((triple11 ((triple12) -> rule3)) -> rule2) OR ((triple11 ((((triple11) -> rule1)) -> rule3)) -> rule2))] Fiona is furry.[(triple9 OR ((triple12) -> rule3) OR ((((triple11) -> rule1)) -> rule3))] Fiona is kind.[(triple11)] Fiona is nice.[(triple12 OR ((triple11) -> rule1))] Fiona is not green.[(triple10)] Fiona is red.[(triple13)] Fiona is smart.[(triple14)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple5) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is not kind.
("Bob" "is" "kind" "-")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
((triple11 triple9) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple11 ((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((triple11 ((((triple11) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
((triple12) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple11
Fiona is nice.
("Fiona" "is" "nice" "+")
triple12
((triple11) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not green.
("Fiona" "is" "green" "-")
triple10
Fiona is red.
("Fiona" "is" "red" "+")
triple13
Fiona is smart.
("Fiona" "is" "smart" "+")
triple14