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