Gary is green. Gary is quiet. Gary is red. Gary is rough. Gary is round. Gary is white. Gary is young. If something is round and red then it is young. If something is young and green then it is quiet. If something is rough and quiet then it is green.
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is round and red then it is young.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is young and green then it is quiet.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is rough and quiet then it is green.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Gary is quiet.
True
1
proof
[(triple2 OR ((triple7 triple1) -> rule2) OR ((((triple5 triple3) -> rule1) triple1) -> rule2))]
("Gary" "is" "quiet" "+")
triple2
((triple7 triple1) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple5 triple3) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not young.
False
1
inv-proof
[(triple7 OR ((triple5 triple3) -> rule1))]
("Gary" "is" "young" "-")
triple7
((triple5 triple3) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
@0: Gary is green.[(triple1 OR ((triple4 triple2) -> rule3))] Gary is quiet.[(triple2 OR ((triple7 triple1) -> rule2) OR ((((triple5 triple3) -> rule1) triple1) -> rule2))] Gary is red.[(triple3)] Gary is rough.[(triple4)] Gary is round.[(triple5)] Gary is white.[(triple6)] Gary is young.[(triple7 OR ((triple5 triple3) -> rule1))]
Gary is green.
("Gary" "is" "green" "+")
triple1
((triple4 triple2) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple2
((triple7 triple1) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple5 triple3) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
((triple5 triple3) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1