Charlie is furry. Charlie is green. Charlie is kind. Charlie is smart. Charlie is white. Charlie is young. Gary is green. Gary is kind. Gary is red. Gary is smart. Gary is white. Gary is young. If Charlie is smart then Charlie is green. All smart, green things are red. If something is red and white then it is green. If Gary is red and Gary is kind then Gary is white. If something is young then it is white. If Gary is white then Gary is green.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If Charlie is smart then Charlie is green.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "green" "+"))
All smart, green things are red.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is red and white then it is green.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If Gary is red and Gary is kind then Gary is white.
((("Gary" "is" "red" "+") ("Gary" "is" "kind" "+")) -> ("Gary" "is" "white" "+"))
If something is young then it is white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If Gary is white then Gary is green.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "green" "+"))
Gary is kind.
True
1
proof
[(triple8)]
("Gary" "is" "kind" "+")
triple8
Gary is not young.
False
1
inv-proof
[(triple12)]
("Gary" "is" "young" "-")
triple12
Charlie is red.
True
3
proof
[(((triple4 triple2) -> rule2) OR ((triple4 ((triple4) -> rule1)) -> rule2))]
("Charlie" "is" "red" "+")
((triple4 triple2) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((triple4 triple2) -> rule2) OR ((triple4 ((triple4) -> rule1)) -> rule2))]
("Charlie" "is" "red" "-")
((triple4 triple2) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
@0: Charlie is furry.[(triple1)] Charlie is green.[(triple2 OR ((triple4) -> rule1))] Charlie is kind.[(triple3)] Charlie is smart.[(triple4)] Charlie is white.[(triple5 OR ((triple6) -> rule5))] Charlie is young.[(triple6)] Gary is green.[(triple7 OR ((triple11) -> rule6) OR ((triple9 triple11) -> rule3) OR ((((triple12) -> rule5)) -> rule6) OR ((((triple9 triple8) -> rule4)) -> rule6) OR ((triple9 ((triple12) -> rule5)) -> rule3) OR ((triple9 ((triple9 triple8) -> rule4)) -> rule3))] Gary is kind.[(triple8)] Gary is red.[(triple9 OR ((triple10 triple7) -> rule2) OR ((triple10 ((triple11) -> rule6)) -> rule2) OR ((triple10 ((((triple12) -> rule5)) -> rule6)) -> rule2))] Gary is smart.[(triple10)] Gary is white.[(triple11 OR ((triple12) -> rule5) OR ((triple9 triple8) -> rule4) OR ((((triple10 triple7) -> rule2) triple8) -> rule4))] Gary is young.[(triple12)] @1: Charlie is red.[(((triple4 triple2) -> rule2) OR ((triple4 ((triple4) -> rule1)) -> rule2))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple4) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple5
((triple6) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple11) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple9 triple11) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple9 triple8) -> (rule4 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple9 ((triple12) -> (rule5 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple9 ((triple9 triple8) -> (rule4 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
((triple10 triple7) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple10 ((triple11) -> (rule6 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((triple10 ((((triple12) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Gary is white.
("Gary" "is" "white" "+")
triple11
((triple12) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple9 triple8) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple10 triple7) -> (rule2 % int2)) triple8) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple12
Charlie is red.
("Charlie" "is" "red" "+")
((triple4 triple2) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2