Bob is big. Bob is blue. Bob is furry. Bob is quiet. Bob is red. Bob is round. Bob is young. Harry is big. Harry is blue. Harry is furry. Harry is quiet. Harry is red. Harry is round. Harry is young. Young people are quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Bob is not blue.
False
1
inv-proof
[(triple2)]
("Bob" "is" "blue" "-")
triple2
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is furry.[(triple3)] Bob is quiet.[(triple4 OR ((triple7) -> rule1))] Bob is red.[(triple5)] Bob is round.[(triple6)] Bob is young.[(triple7)] Harry is big.[(triple8)] Harry is blue.[(triple9)] Harry is furry.[(triple10)] Harry is quiet.[(triple11 OR ((triple14) -> rule1))] Harry is red.[(triple12)] Harry is round.[(triple13)] Harry is young.[(triple14)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple7) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
((triple14) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14