Bob is not big. Bob is cold. Bob is furry. Bob is quiet. Bob is round. Bob is white. Bob is young. Dave is big. Dave is cold. Dave is furry. Dave is quiet. Dave is round. Dave is white. Dave is young. If Dave is quiet and Dave is furry then Dave is round. Round people are quiet. If Bob is big and Bob is not quiet then Bob is cold.
Bob is not big.
("Bob" "is" "big" "-")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
If Dave is quiet and Dave is furry then Dave is round.
((("Dave" "is" "quiet" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "round" "+"))
Round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is big and Bob is not quiet then Bob is cold.
((("Bob" "is" "big" "+") ("Bob" "is" "quiet" "~")) -> ("Bob" "is" "cold" "+"))
Bob is not big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Dave is not cold.
False
1
inv-proof
[(triple9)]
("Dave" "is" "cold" "-")
triple9
@0: Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is not big.[(triple1)] Bob is quiet.[(triple4 OR ((triple5) -> rule2))] Bob is round.[(triple5)] Bob is white.[(triple6)] Bob is young.[(triple7)] Dave is big.[(triple8)] Dave is cold.[(triple9)] Dave is furry.[(triple10)] Dave is quiet.[(triple11 OR ((triple12) -> rule2))] Dave is round.[(triple12 OR ((triple11 triple10) -> rule1))] Dave is white.[(triple13)] Dave is young.[(triple14)]
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple5) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is furry.
("Dave" "is" "furry" "+")
triple10
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
((triple12) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple12
((triple11 triple10) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple13
Dave is young.
("Dave" "is" "young" "+")
triple14