Bob is big. Bob is nice. Bob is red. Bob is rough. Bob is round. Bob is white. Bob is young. Charlie is big. Charlie is nice. Charlie is red. Charlie is rough. Charlie is round. Charlie is white. Charlie is young. If someone is rough and round then they are young. Red, young people are nice. All young people are rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
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" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If someone is rough and round then they are young.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Red, young people are nice.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
All young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
Bob is young.
True
1
proof
[(triple7 OR ((triple4 triple5) -> rule1))]
("Bob" "is" "young" "+")
triple7
((triple4 triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is not rough.
False
1
inv-proof
[(triple11 OR ((triple14) -> rule3))]
("Charlie" "is" "rough" "-")
triple11
((triple14) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
@0: Bob is big.[(triple1)] Bob is nice.[(triple2 OR ((triple3 triple7) -> rule2) OR ((triple3 ((triple4 triple5) -> rule1)) -> rule2))] Bob is red.[(triple3)] Bob is rough.[(triple4 OR ((triple7) -> rule3))] Bob is round.[(triple5)] Bob is white.[(triple6)] Bob is young.[(triple7 OR ((triple4 triple5) -> rule1))] Charlie is big.[(triple8)] Charlie is nice.[(triple9 OR ((triple10 triple14) -> rule2) OR ((triple10 ((triple11 triple12) -> rule1)) -> rule2))] Charlie is red.[(triple10)] Charlie is rough.[(triple11 OR ((triple14) -> rule3))] Charlie is round.[(triple12)] Charlie is white.[(triple13)] Charlie is young.[(triple14 OR ((triple11 triple12) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((triple3 triple7) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple3 ((triple4 triple5) -> (rule1 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple7) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple4 triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple8
Charlie is nice.
("Charlie" "is" "nice" "+")
triple9
((triple10 triple14) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple10 ((triple11 triple12) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
((triple14) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple12
Charlie is white.
("Charlie" "is" "white" "+")
triple13
Charlie is young.
("Charlie" "is" "young" "+")
triple14
((triple11 triple12) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1