Gary is blue. Gary is cold. Gary is green. Gary is rough. Gary is round. Gary is smart. Gary is young. Cold people are blue. All blue, cold people are green. All blue, cold people are round. All smart people are rough. If someone is cold and green then they are round. All blue, green people are young.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
All blue, cold people are green.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
All blue, cold people are round.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and green then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
All blue, green people are young.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Gary is young.
True
1
proof
[(triple7 OR ((triple1 triple3) -> rule6) OR ((triple1 ((triple1 triple2) -> rule2)) -> rule6) OR ((((triple2) -> rule1) triple3) -> rule6) OR ((((triple2) -> rule1) ((triple1 triple2) -> rule2)) -> rule6) OR ((triple1 ((((triple2) -> rule1) triple2) -> rule2)) -> rule6) OR ((((triple2) -> rule1) ((((triple2) -> rule1) triple2) -> rule2)) -> rule6))]
("Gary" "is" "young" "+")
triple7
((triple1 triple3) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple1 ((triple1 triple2) -> (rule2 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple2) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple2) -> (rule1 % int3)) ((triple1 triple2) -> (rule2 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((triple1 ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is not rough.
False
1
inv-proof
[(triple4 OR ((triple6) -> rule4))]
("Gary" "is" "rough" "-")
triple4
((triple6) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
@0: Gary is blue.[(triple1 OR ((triple2) -> rule1))] Gary is cold.[(triple2)] Gary is green.[(triple3 OR ((triple1 triple2) -> rule2) OR ((((triple2) -> rule1) triple2) -> rule2))] Gary is rough.[(triple4 OR ((triple6) -> rule4))] Gary is round.[(triple5 OR ((triple1 triple2) -> rule3) OR ((triple2 triple3) -> rule5) OR ((triple2 ((triple1 triple2) -> rule2)) -> rule5) OR ((((triple2) -> rule1) triple2) -> rule3) OR ((triple2 ((((triple2) -> rule1) triple2) -> rule2)) -> rule5))] Gary is smart.[(triple6)] Gary is young.[(triple7 OR ((triple1 triple3) -> rule6) OR ((triple1 ((triple1 triple2) -> rule2)) -> rule6) OR ((((triple2) -> rule1) triple3) -> rule6) OR ((((triple2) -> rule1) ((triple1 triple2) -> rule2)) -> rule6) OR ((triple1 ((((triple2) -> rule1) triple2) -> rule2)) -> rule6) OR ((((triple2) -> rule1) ((((triple2) -> rule1) triple2) -> rule2)) -> rule6))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
((triple2) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
((triple1 triple2) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple4
((triple6) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple5
((triple1 triple2) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple2 triple3) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple2 ((triple1 triple2) -> (rule2 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple2 ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
((triple1 triple3) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple1 ((triple1 triple2) -> (rule2 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple2) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple2) -> (rule1 % int3)) ((triple1 triple2) -> (rule2 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((triple1 ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3