Charlie is big. Charlie is blue. Charlie is green. Charlie is kind. Charlie is red. Charlie is round. Charlie is not young. Dave is big. Dave is blue. Dave is not green. Dave is not kind. Dave is red. Dave is round. Dave is young. If Dave is green then Dave is young. Blue people are red.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
If Dave is green then Dave is young.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "young" "+"))
Blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Dave is big.
True
1
proof
[(triple8)]
("Dave" "is" "big" "+")
triple8
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is green.[(triple3)] Charlie is kind.[(triple4)] Charlie is not young.[(triple7)] Charlie is red.[(triple5 OR ((triple2) -> rule2))] Charlie is round.[(triple6)] Dave is big.[(triple8)] Dave is blue.[(triple9)] Dave is not green.[(triple10)] Dave is not kind.[(triple11)] Dave is red.[(triple12 OR ((triple9) -> rule2))] Dave is round.[(triple13)] Dave is young.[(triple14)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is not young.
("Charlie" "is" "young" "-")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((triple2) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is not green.
("Dave" "is" "green" "-")
triple10
Dave is not kind.
("Dave" "is" "kind" "-")
triple11
Dave is red.
("Dave" "is" "red" "+")
triple12
((triple9) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple13
Dave is young.
("Dave" "is" "young" "+")
triple14