Gary is big. Gary is green. Gary is rough. Nice people are white. All blue, white people are kind. If Gary is kind and Gary is rough then Gary is blue. Nice, white people are big. If someone is white then they are blue. If someone is green and rough then they are white.
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
All blue, white people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If Gary is kind and Gary is rough then Gary is blue.
((("Gary" "is" "kind" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "blue" "+"))
Nice, white people are big.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is white then they are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is green and rough then they are white.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Gary is green.
True
1
proof
[(triple2)]
("Gary" "is" "green" "+")
triple2
Gary is not green.
False
1
inv-proof
[(triple2)]
("Gary" "is" "green" "-")
triple2
Gary is white.
True
3
proof
[(((triple2 triple3) -> rule6))]
("Gary" "is" "white" "+")
((triple2 triple3) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
3
inv-proof
[(((triple2 triple3) -> rule6))]
("Gary" "is" "white" "-")
((triple2 triple3) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
True
4
proof
[(((((triple2 triple3) -> rule6)) -> rule5))]
("Gary" "is" "blue" "+")
((((triple2 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not blue.
False
4
inv-proof
[(((((triple2 triple3) -> rule6)) -> rule5))]
("Gary" "is" "blue" "-")
((((triple2 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
True
8
proof
[(((((((triple2 triple3) -> rule6)) -> rule5) ((triple2 triple3) -> rule6)) -> rule2))]
("Gary" "is" "kind" "+")
((((((triple2 triple3) -> (rule6 % int3))) -> (rule5 % int2)) ((triple2 triple3) -> (rule6 % int3))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not kind.
False
8
inv-proof
[(((((((triple2 triple3) -> rule6)) -> rule5) ((triple2 triple3) -> rule6)) -> rule2))]
("Gary" "is" "kind" "-")
((((((triple2 triple3) -> (rule6 % int3))) -> (rule5 % int2)) ((triple2 triple3) -> (rule6 % int3))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
@0: Gary is big.[(triple1)] Gary is green.[(triple2)] Gary is rough.[(triple3)] @1: Gary is white.[(((triple2 triple3) -> rule6))] @2: Gary is blue.[(((((triple2 triple3) -> rule6)) -> rule5))] @3: Gary is kind.[(((((((triple2 triple3) -> rule6)) -> rule5) ((triple2 triple3) -> rule6)) -> rule2))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Gary is white.
("Gary" "is" "white" "+")
((triple2 triple3) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple2 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple2 triple3) -> (rule6 % int3))) -> (rule5 % int2)) ((triple2 triple3) -> (rule6 % int3))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3