Gary is not red. Gary is not white. Gary is young. Red, young people are big. If someone is young then they are big. If Gary is red then Gary is not big. Young people are rough. All nice, big people are young. If Gary is young and Gary is not white then Gary is rough. All young, big people are not nice. If someone is big and not round then they are red.
Gary is not red.
("Gary" "is" "red" "-")
Gary is not white.
("Gary" "is" "white" "-")
Gary is young.
("Gary" "is" "young" "+")
Red, young people are big.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is young then they are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If Gary is red then Gary is not big.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "big" "-"))
Young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
All nice, big people are young.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If Gary is young and Gary is not white then Gary is rough.
((("Gary" "is" "young" "+") ("Gary" "is" "white" "~")) -> ("Gary" "is" "rough" "+"))
All young, big people are not nice.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "-"))
If someone is big and not round then they are red.
((("someone" "is" "big" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "red" "+"))
Gary is not red.
True
1
proof
[(triple1)]
("Gary" "is" "red" "-")
triple1
Gary is white.
False
1
inv-proof
[(triple2)]
("Gary" "is" "white" "+")
triple2
Gary is rough.
True
2
proof
[(((triple3) -> rule4) OR ((triple3 triple2) -> rule6))]
("Gary" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple3 triple2) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple3) -> rule4) OR ((triple3 triple2) -> rule6))]
("Gary" "is" "rough" "-")
((triple3) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple3 triple2) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not nice.
True
4
proof
[(((triple3 ((triple3) -> rule2)) -> rule7))]
("Gary" "is" "nice" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule7))]
("Gary" "is" "nice" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
@0: Gary is not red.[(triple1)] Gary is not white.[(triple2)] Gary is young.[(triple3)] @1: Gary is big.[(((triple3) -> rule2))] Gary is rough.[(((triple3) -> rule4) OR ((triple3 triple2) -> rule6))] @2: Gary is not nice.[(((triple3 ((triple3) -> rule2)) -> rule7))]
Gary is not red.
("Gary" "is" "red" "-")
triple1
Gary is not white.
("Gary" "is" "white" "-")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
((triple3) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple3 triple2) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2