Anne is big. Anne is blue. Anne is green. Anne is quiet. Anne is red. Anne is white. Anne is young. Dave is big. Dave is blue. Dave is green. Dave is quiet. Dave is red. Dave is white. Dave is young. Red, big things are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Red, big things are quiet.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Anne is white.
True
1
proof
[(triple6)]
("Anne" "is" "white" "+")
triple6
Dave is not red.
False
1
inv-proof
[(triple12)]
("Dave" "is" "red" "-")
triple12
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is green.[(triple3)] Anne is quiet.[(triple4 OR ((triple5 triple1) -> rule1))] Anne is red.[(triple5)] Anne is white.[(triple6)] Anne is young.[(triple7)] Dave is big.[(triple8)] Dave is blue.[(triple9)] Dave is green.[(triple10)] Dave is quiet.[(triple11 OR ((triple12 triple8) -> rule1))] Dave is red.[(triple12)] Dave is white.[(triple13)] Dave is young.[(triple14)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple5 triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is green.
("Dave" "is" "green" "+")
triple10
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
((triple12 triple8) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple12
Dave is white.
("Dave" "is" "white" "+")
triple13
Dave is young.
("Dave" "is" "young" "+")
triple14