Gary is cold. Gary is white. Gary is young. All rough things are not big. Young things are blue. If something is rough and big then it is not blue. Young, cold things are white. If something is rough then it is red. All cold, blue things are rough. If Gary is blue and Gary is not rough then Gary is white. If Gary is big and Gary is not young then Gary is not white.
Gary is cold.
("Gary" "is" "cold" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All rough things are not big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "-"))
Young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is rough and big then it is not blue.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "-"))
Young, cold things are white.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is rough then it is red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All cold, blue things are rough.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If Gary is blue and Gary is not rough then Gary is white.
((("Gary" "is" "blue" "+") ("Gary" "is" "rough" "~")) -> ("Gary" "is" "white" "+"))
If Gary is big and Gary is not young then Gary is not white.
((("Gary" "is" "big" "+") ("Gary" "is" "young" "~")) -> ("Gary" "is" "white" "-"))
Gary is cold.
True
1
proof
[(triple1)]
("Gary" "is" "cold" "+")
triple1
Gary is not white.
False
1
inv-proof
[(triple2 OR ((triple3 triple1) -> rule4))]
("Gary" "is" "white" "-")
triple2
((triple3 triple1) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
True
4
proof
[(((triple1 ((triple3) -> rule2)) -> rule6))]
("Gary" "is" "rough" "+")
((triple1 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not rough.
False
4
inv-proof
[(((triple1 ((triple3) -> rule2)) -> rule6))]
("Gary" "is" "rough" "-")
((triple1 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
True
5
proof
[(((((triple1 ((triple3) -> rule2)) -> rule6)) -> rule5))]
("Gary" "is" "red" "+")
((((triple1 ((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is big.
False
5
inv-proof
[(((((triple1 ((triple3) -> rule2)) -> rule6)) -> rule1))]
("Gary" "is" "big" "+")
((((triple1 ((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
@0: Gary is cold.[(triple1)] Gary is white.[(triple2 OR ((triple3 triple1) -> rule4))] Gary is young.[(triple3)] @1: Gary is blue.[(((triple3) -> rule2))] @2: Gary is rough.[(((triple1 ((triple3) -> rule2)) -> rule6))] @3: Gary is not big.[(((((triple1 ((triple3) -> rule2)) -> rule6)) -> rule1))] Gary is red.[(((((triple1 ((triple3) -> rule2)) -> rule6)) -> rule5))]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
Gary is white.
("Gary" "is" "white" "+")
triple2
((triple3 triple1) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple1 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not big.
("Gary" "is" "big" "-")
((((triple1 ((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((triple1 ((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3