Gary is kind. If something is nice and rough then it is white. Blue things are green. All blue, young things are rough. If Gary is rough then Gary is blue. Blue things are white. Kind things are white. If Gary is white and Gary is young then Gary is rough. All kind things are young.
Gary is kind.
("Gary" "is" "kind" "+")
If something is nice and rough then it is white.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
All blue, young things are rough.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If Gary is rough then Gary is blue.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "blue" "+"))
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If Gary is white and Gary is young then Gary is rough.
((("Gary" "is" "white" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "rough" "+"))
All kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Gary is kind.
True
1
proof
[(triple1)]
("Gary" "is" "kind" "+")
triple1
Gary is not kind.
False
1
inv-proof
[(triple1)]
("Gary" "is" "kind" "-")
triple1
Gary is white.
True
2
proof
[(((triple1) -> rule6))]
("Gary" "is" "white" "+")
((triple1) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple1) -> rule8))]
("Gary" "is" "young" "-")
((triple1) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
True
5
proof
[(((((triple1) -> rule6) ((triple1) -> rule8)) -> rule7))]
("Gary" "is" "rough" "+")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not rough.
False
5
inv-proof
[(((((triple1) -> rule6) ((triple1) -> rule8)) -> rule7))]
("Gary" "is" "rough" "-")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is blue.
True
6
proof
[(((((((triple1) -> rule6) ((triple1) -> rule8)) -> rule7)) -> rule4))]
("Gary" "is" "blue" "+")
((((((triple1) -> (rule6 % int4)) ((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is not blue.
False
6
inv-proof
[(((((((triple1) -> rule6) ((triple1) -> rule8)) -> rule7)) -> rule4))]
("Gary" "is" "blue" "-")
((((((triple1) -> (rule6 % int4)) ((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
@0: Gary is kind.[(triple1)] @1: Gary is white.[(((triple1) -> rule6))] Gary is young.[(((triple1) -> rule8))] @2: Gary is rough.[(((((triple1) -> rule6) ((triple1) -> rule8)) -> rule7))] @3: Gary is blue.[(((((((triple1) -> rule6) ((triple1) -> rule8)) -> rule7)) -> rule4))] @4: Gary is green.[(((((((((triple1) -> rule6) ((triple1) -> rule8)) -> rule7)) -> rule4)) -> rule2))]
Gary is kind.
("Gary" "is" "kind" "+")
triple1
Gary is white.
("Gary" "is" "white" "+")
((triple1) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple1) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple1) -> (rule6 % int4)) ((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is green.
("Gary" "is" "green" "+")
((((((((triple1) -> (rule6 % int5)) ((triple1) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
int5