Bob is big. Bob is cold. Bob is furry. Bob is green. Bob is quiet. Bob is red. Bob is round. All cold, green things are quiet. All green things are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
All cold, green things are quiet.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
All green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
Bob is round.
True
1
proof
[(triple7)]
("Bob" "is" "round" "+")
triple7
Bob is not big.
False
1
inv-proof
[(triple1 OR ((triple4) -> rule2))]
("Bob" "is" "big" "-")
triple1
((triple4) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
@0: Bob is big.[(triple1 OR ((triple4) -> rule2))] Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is green.[(triple4)] Bob is quiet.[(triple5 OR ((triple2 triple4) -> rule1))] Bob is red.[(triple6)] Bob is round.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple4) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple2 triple4) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple6
Bob is round.
("Bob" "is" "round" "+")
triple7