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