Anne is big. Anne is furry. Anne is green. Anne is kind. Anne is round. Anne is smart. Anne is white. Dave is big. Dave is furry. Dave is green. Dave is kind. Dave is round. Dave is smart. Dave is white. If something is smart then it is kind.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
If something is smart then it is kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Anne is white.
True
1
proof
[(triple7)]
("Anne" "is" "white" "+")
triple7
Dave is not white.
False
1
inv-proof
[(triple14)]
("Dave" "is" "white" "-")
triple14
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is green.[(triple3)] Anne is kind.[(triple4 OR ((triple6) -> rule1))] Anne is round.[(triple5)] Anne is smart.[(triple6)] Anne is white.[(triple7)] Dave is big.[(triple8)] Dave is furry.[(triple9)] Dave is green.[(triple10)] Dave is kind.[(triple11 OR ((triple13) -> rule1))] Dave is round.[(triple12)] Dave is smart.[(triple13)] Dave is white.[(triple14)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
((triple6) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Anne is white.
("Anne" "is" "white" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is green.
("Dave" "is" "green" "+")
triple10
Dave is kind.
("Dave" "is" "kind" "+")
triple11
((triple13) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple12
Dave is smart.
("Dave" "is" "smart" "+")
triple13
Dave is white.
("Dave" "is" "white" "+")
triple14