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