Bob is green. Bob is kind. Bob is nice. Bob is quiet. Bob is red. Bob is rough. Bob is young. Charlie is green. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is rough. Charlie is young. If Charlie is nice and Charlie is young then Charlie is green. All young, green people are nice.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If Charlie is nice and Charlie is young then Charlie is green.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "green" "+"))
All young, green people are nice.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Charlie is nice.
True
1
proof
[(triple10 OR ((triple14 triple8) -> rule2))]
("Charlie" "is" "nice" "+")
triple10
((triple14 triple8) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not rough.
False
1
inv-proof
[(triple13)]
("Charlie" "is" "rough" "-")
triple13
@0: Bob is green.[(triple1)] Bob is kind.[(triple2)] Bob is nice.[(triple3 OR ((triple7 triple1) -> rule2))] Bob is quiet.[(triple4)] Bob is red.[(triple5)] Bob is rough.[(triple6)] Bob is young.[(triple7)] Charlie is green.[(triple8 OR ((triple10 triple14) -> rule1))] Charlie is kind.[(triple9)] Charlie is nice.[(triple10 OR ((triple14 triple8) -> rule2))] Charlie is quiet.[(triple11)] Charlie is red.[(triple12)] Charlie is rough.[(triple13)] Charlie is young.[(triple14)]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple7 triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
((triple10 triple14) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
Charlie is nice.
("Charlie" "is" "nice" "+")
triple10
((triple14 triple8) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple11
Charlie is red.
("Charlie" "is" "red" "+")
triple12
Charlie is rough.
("Charlie" "is" "rough" "+")
triple13
Charlie is young.
("Charlie" "is" "young" "+")
triple14