Bob is big. Bob is kind. Bob is not nice. Bob is rough. Bob is smart. Bob is white. Bob is not young. If something is young then it is nice. If something is rough and young then it is not white. All white things are kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not 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 something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is rough and young then it is not white.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "-"))
All white things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Bob is not young.
True
1
proof
[(triple7)]
("Bob" "is" "young" "-")
triple7
Bob is not white.
False
1
inv-proof
[(triple6)]
("Bob" "is" "white" "-")
triple6
@0: Bob is big.[(triple1)] Bob is kind.[(triple2 OR ((triple6) -> rule3))] Bob is not nice.[(triple3)] Bob is not young.[(triple7)] Bob is rough.[(triple4)] Bob is smart.[(triple5)] Bob is white.[(triple6)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
((triple6) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
triple3
Bob is not young.
("Bob" "is" "young" "-")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6