Bob is furry. Bob is green. Bob is nice. Bob is rough. Bob is smart. Bob is white. Bob is not young. If someone is nice and green then they are not young. If someone is smart and rough then they are white. If Bob is smart then Bob is furry.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is not young.
("Bob" "is" "young" "-")
If someone is nice and green then they are not young.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "-"))
If someone is smart and rough then they are white.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If Bob is smart then Bob is furry.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "furry" "+"))
Bob is smart.
True
1
proof
[(triple5)]
("Bob" "is" "smart" "+")
triple5
Bob is not smart.
False
1
inv-proof
[(triple5)]
("Bob" "is" "smart" "-")
triple5
@0: Bob is furry.[(triple1 OR ((triple5) -> rule3))] Bob is green.[(triple2)] Bob is nice.[(triple3)] Bob is not young.[(triple7 OR ((triple3 triple2) -> rule1))] Bob is rough.[(triple4)] Bob is smart.[(triple5)] Bob is white.[(triple6 OR ((triple5 triple4) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
((triple5) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not young.
("Bob" "is" "young" "-")
triple7
((triple3 triple2) -> (rule1 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple5 triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1