Bob is big. Bob is furry. Bob is green. Bob is nice. Bob is quiet. Bob is rough. Bob is round. Dave is big. Dave is furry. Dave is green. Dave is nice. Dave is quiet. Dave is rough. Dave is round. All furry things are quiet. All green things are furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
All furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
All green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Dave is big.
True
1
proof
[(triple8)]
("Dave" "is" "big" "+")
triple8
Dave is not quiet.
False
1
inv-proof
[(triple12 OR ((triple9) -> rule1) OR ((((triple10) -> rule2)) -> rule1))]
("Dave" "is" "quiet" "-")
triple12
((triple9) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
@0: Bob is big.[(triple1)] Bob is furry.[(triple2 OR ((triple3) -> rule2))] Bob is green.[(triple3)] Bob is nice.[(triple4)] Bob is quiet.[(triple5 OR ((triple2) -> rule1) OR ((((triple3) -> rule2)) -> rule1))] Bob is rough.[(triple6)] Bob is round.[(triple7)] Dave is big.[(triple8)] Dave is furry.[(triple9 OR ((triple10) -> rule2))] Dave is green.[(triple10)] Dave is nice.[(triple11)] Dave is quiet.[(triple12 OR ((triple9) -> rule1) OR ((((triple10) -> rule2)) -> rule1))] Dave is rough.[(triple13)] Dave is round.[(triple14)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple3) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Bob is round.
("Bob" "is" "round" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple9
((triple10) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
triple11
Dave is quiet.
("Dave" "is" "quiet" "+")
triple12
((triple9) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
triple13
Dave is round.
("Dave" "is" "round" "+")
triple14