Bob is big. Bob is blue. Bob is kind. Bob is nice. Bob is red. Bob is white. Bob is young. Big, nice people are kind. All red, kind people are white. If someone is kind then they are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Big, nice people are kind.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All red, kind people are white.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Bob is white.
True
1
proof
[(triple6 OR ((triple5 triple3) -> rule2) OR ((triple5 ((triple1 triple4) -> rule1)) -> rule2))]
("Bob" "is" "white" "+")
triple6
((triple5 triple3) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple5 ((triple1 triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not young.
False
1
inv-proof
[(triple7)]
("Bob" "is" "young" "-")
triple7
@0: Bob is big.[(triple1 OR ((triple3) -> rule3))] Bob is blue.[(triple2)] Bob is kind.[(triple3 OR ((triple1 triple4) -> rule1))] Bob is nice.[(triple4)] Bob is red.[(triple5)] Bob is white.[(triple6 OR ((triple5 triple3) -> rule2) OR ((triple5 ((triple1 triple4) -> rule1)) -> rule2))] Bob is young.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple1 triple4) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple5 triple3) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple5 ((triple1 triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple7