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