Gary is blue. Gary is green. Gary is kind. Gary is quiet. Gary is red. Gary is rough. Gary is round. Green, round people are red. Green, quiet people are blue. If someone is quiet and rough then they are round.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Green, round people are red.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Green, quiet people are blue.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet and rough then they are round.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
Gary is round.
True
1
proof
[(triple7 OR ((triple4 triple6) -> rule3))]
("Gary" "is" "round" "+")
triple7
((triple4 triple6) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is not rough.
False
1
inv-proof
[(triple6)]
("Gary" "is" "rough" "-")
triple6
@0: Gary is blue.[(triple1 OR ((triple2 triple4) -> rule2))] Gary is green.[(triple2)] Gary is kind.[(triple3)] Gary is quiet.[(triple4)] Gary is red.[(triple5 OR ((triple2 triple7) -> rule1) OR ((triple2 ((triple4 triple6) -> rule3)) -> rule1))] Gary is rough.[(triple6)] Gary is round.[(triple7 OR ((triple4 triple6) -> rule3))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
((triple2 triple4) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
((triple2 triple7) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple2 ((triple4 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
((triple4 triple6) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1