Anne is big. Anne is blue. Anne is cold. Anne is furry. Anne is quiet. Anne is red. Anne is round. Bob is big. Bob is blue. Bob is cold. Bob is furry. Bob is not quiet. Bob is not red. Bob is not round. All blue things are furry. All round things are big. If Bob is furry and Bob is round then Bob is quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is not red.
("Bob" "is" "red" "-")
Bob is not round.
("Bob" "is" "round" "-")
All blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Bob is furry and Bob is round then Bob is quiet.
((("Bob" "is" "furry" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "quiet" "+"))
Bob is not round.
True
1
proof
[(triple14)]
("Bob" "is" "round" "-")
triple14
Bob is round.
False
1
inv-proof
[(triple14)]
("Bob" "is" "round" "+")
triple14
@0: Anne is big.[(triple1 OR ((triple7) -> rule2))] Anne is blue.[(triple2)] Anne is cold.[(triple3)] Anne is furry.[(triple4 OR ((triple2) -> rule1))] Anne is quiet.[(triple5)] Anne is red.[(triple6)] Anne is round.[(triple7)] Bob is big.[(triple8)] Bob is blue.[(triple9)] Bob is cold.[(triple10)] Bob is furry.[(triple11 OR ((triple9) -> rule1))] Bob is not quiet.[(triple12)] Bob is not red.[(triple13)] Bob is not round.[(triple14)]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple7) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is furry.
("Anne" "is" "furry" "+")
triple4
((triple2) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Anne is red.
("Anne" "is" "red" "+")
triple6
Anne is round.
("Anne" "is" "round" "+")
triple7
Bob is big.
("Bob" "is" "big" "+")
triple8
Bob is blue.
("Bob" "is" "blue" "+")
triple9
Bob is cold.
("Bob" "is" "cold" "+")
triple10
Bob is furry.
("Bob" "is" "furry" "+")
triple11
((triple9) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple12
Bob is not red.
("Bob" "is" "red" "-")
triple13
Bob is not round.
("Bob" "is" "round" "-")
triple14