Bob is furry. Bob is green. Bob is smart. Harry is furry. Harry is not green. Harry is kind. Harry is red. Harry is rough. Harry is smart. Harry is white. If someone is rough and green then they are white. If someone is rough and furry then they are red. All smart, green people are rough.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is rough and green then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If someone is rough and furry then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All smart, green people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Harry is green.
False
1
inv-proof
[(triple5)]
("Harry" "is" "green" "+")
triple5
Bob is rough.
True
3
proof
[(((triple3 triple2) -> rule3))]
("Bob" "is" "rough" "+")
((triple3 triple2) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
3
inv-proof
[(((triple3 triple2) -> rule3))]
("Bob" "is" "rough" "-")
((triple3 triple2) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
True
5
proof
[(((((triple3 triple2) -> rule3) triple1) -> rule2))]
("Bob" "is" "red" "+")
((((triple3 triple2) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not white.
False
5
inv-proof
[(((((triple3 triple2) -> rule3) triple2) -> rule1))]
("Bob" "is" "white" "-")
((((triple3 triple2) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
@0: Bob is furry.[(triple1)] Bob is green.[(triple2)] Bob is smart.[(triple3)] Harry is furry.[(triple4)] Harry is kind.[(triple6)] Harry is not green.[(triple5)] Harry is red.[(triple7 OR ((triple8 triple4) -> rule2))] Harry is rough.[(triple8)] Harry is smart.[(triple9)] Harry is white.[(triple10)] @1: Bob is rough.[(((triple3 triple2) -> rule3))] @2: Bob is red.[(((((triple3 triple2) -> rule3) triple1) -> rule2))] Bob is white.[(((((triple3 triple2) -> rule3) triple2) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is not green.
("Harry" "is" "green" "-")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple7
((triple8 triple4) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Bob is rough.
("Bob" "is" "rough" "+")
((triple3 triple2) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple3 triple2) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple3 triple2) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2