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