Gary is big. Gary is green. Gary is not round. If someone is green and furry then they are red. All big, round people are red. All big, quiet people are red. If Gary is red and Gary is quiet then Gary is green. If someone is green and not round then they are furry. Green, red people are young. If someone is furry and red then they are green. If Gary is quiet and Gary is not red then Gary is not young.
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is not round.
("Gary" "is" "round" "-")
If someone is green and furry then they are red.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All big, round people are red.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All big, quiet people are red.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If Gary is red and Gary is quiet then Gary is green.
((("Gary" "is" "red" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "green" "+"))
If someone is green and not round then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "furry" "+"))
Green, red people are young.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is furry and red then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If Gary is quiet and Gary is not red then Gary is not young.
((("Gary" "is" "quiet" "+") ("Gary" "is" "red" "~")) -> ("Gary" "is" "young" "-"))
Gary is big.
True
1
proof
[(triple1)]
("Gary" "is" "big" "+")
triple1
Gary is round.
False
1
inv-proof
[(triple3)]
("Gary" "is" "round" "+")
triple3
Gary is furry.
True
3
proof
[(((triple2 triple3) -> rule5))]
("Gary" "is" "furry" "+")
((triple2 triple3) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not furry.
False
3
inv-proof
[(((triple2 triple3) -> rule5))]
("Gary" "is" "furry" "-")
((triple2 triple3) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
True
5
proof
[(((triple2 ((triple2 triple3) -> rule5)) -> rule1))]
("Gary" "is" "red" "+")
((triple2 ((triple2 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not red.
False
5
inv-proof
[(((triple2 ((triple2 triple3) -> rule5)) -> rule1))]
("Gary" "is" "red" "-")
((triple2 ((triple2 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
True
7
proof
[(((triple2 ((triple2 ((triple2 triple3) -> rule5)) -> rule1)) -> rule6))]
("Gary" "is" "young" "+")
((triple2 ((triple2 ((triple2 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not young.
False
7
inv-proof
[(((triple2 ((triple2 ((triple2 triple3) -> rule5)) -> rule1)) -> rule6))]
("Gary" "is" "young" "-")
((triple2 ((triple2 ((triple2 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
@0: Gary is big.[(triple1)] Gary is green.[(triple2)] Gary is not round.[(triple3)] @1: Gary is furry.[(((triple2 triple3) -> rule5))] @2: Gary is red.[(((triple2 ((triple2 triple3) -> rule5)) -> rule1))] @3: Gary is young.[(((triple2 ((triple2 ((triple2 triple3) -> rule5)) -> rule1)) -> rule6))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is not round.
("Gary" "is" "round" "-")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
((triple2 triple3) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple2 ((triple2 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple2 ((triple2 ((triple2 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3