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