Charlie is blue. Charlie is green. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is not smart. Charlie is not white. Gary is blue. Gary is green. Gary is nice. Gary is quiet. Gary is red. Gary is smart. Gary is not white. All red, smart things are blue. All green things are red. If Gary is red then Gary is green.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Charlie is not white.
("Charlie" "is" "white" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is not white.
("Gary" "is" "white" "-")
All red, smart things are blue.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If Gary is red then Gary is green.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "green" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Gary is not green.
False
1
inv-proof
[(triple9 OR ((triple12) -> rule3))]
("Gary" "is" "green" "-")
triple9
((triple12) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
@0: Charlie is blue.[(triple1)] Charlie is green.[(triple2)] Charlie is nice.[(triple3)] Charlie is not smart.[(triple6)] Charlie is not white.[(triple7)] Charlie is quiet.[(triple4)] Charlie is red.[(triple5 OR ((triple2) -> rule2))] Gary is blue.[(triple8 OR ((triple12 triple13) -> rule1) OR ((((triple9) -> rule2) triple13) -> rule1))] Gary is green.[(triple9 OR ((triple12) -> rule3))] Gary is nice.[(triple10)] Gary is not white.[(triple14)] Gary is quiet.[(triple11)] Gary is red.[(triple12 OR ((triple9) -> rule2))] Gary is smart.[(triple13)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple6
Charlie is not white.
("Charlie" "is" "white" "-")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((triple2) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple8
((triple12 triple13) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple9) -> (rule2 % int2)) triple13) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple9
((triple12) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is not white.
("Gary" "is" "white" "-")
triple14
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Gary is red.
("Gary" "is" "red" "+")
triple12
((triple9) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple13