Gary is blue. Gary is cold. Gary is furry. Gary is green. Gary is quiet. Gary is round. Gary is young. All green, young things are blue. If something is blue and cold then it is green. Young, round things are blue. If something is blue then it is green. If Gary is cold then Gary is green. If something is young and furry then it is cold. If something is furry then it is cold. If Gary is green then Gary is round.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All green, young things are blue.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is blue and cold then it is green.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Young, round things are blue.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If Gary is cold then Gary is green.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "green" "+"))
If something is young and furry then it is cold.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If Gary is green then Gary is round.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "round" "+"))
Gary is young.
True
1
proof
[(triple7)]
("Gary" "is" "young" "+")
triple7
Gary is not blue.
False
1
inv-proof
[(triple1 OR ((triple4 triple7) -> rule1) OR ((triple7 triple6) -> rule3) OR ((triple7 ((triple4) -> rule8)) -> rule3) OR ((((triple2) -> rule5) triple7) -> rule1) OR ((triple7 ((((triple2) -> rule5)) -> rule8)) -> rule3) OR ((((((triple3) -> rule7)) -> rule5) triple7) -> rule1) OR ((((((triple7 triple3) -> rule6)) -> rule5) triple7) -> rule1) OR ((triple7 ((((((triple3) -> rule7)) -> rule5)) -> rule8)) -> rule3) OR ((triple7 ((((((triple7 triple3) -> rule6)) -> rule5)) -> rule8)) -> rule3))]
("Gary" "is" "blue" "-")
triple1
((triple4 triple7) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple7 triple6) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple7 ((triple4) -> (rule8 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple2) -> (rule5 % int2)) triple7) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((triple7 ((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2)) triple7) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((((triple7 triple3) -> (rule6 % int3))) -> (rule5 % int2)) triple7) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple7 ((((((triple3) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
((triple7 ((((((triple7 triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
@0: Gary is blue.[(triple1 OR ((triple4 triple7) -> rule1) OR ((triple7 triple6) -> rule3) OR ((triple7 ((triple4) -> rule8)) -> rule3) OR ((((triple2) -> rule5) triple7) -> rule1) OR ((triple7 ((((triple2) -> rule5)) -> rule8)) -> rule3) OR ((((((triple3) -> rule7)) -> rule5) triple7) -> rule1) OR ((((((triple7 triple3) -> rule6)) -> rule5) triple7) -> rule1) OR ((triple7 ((((((triple3) -> rule7)) -> rule5)) -> rule8)) -> rule3) OR ((triple7 ((((((triple7 triple3) -> rule6)) -> rule5)) -> rule8)) -> rule3))] Gary is cold.[(triple2 OR ((triple3) -> rule7) OR ((triple7 triple3) -> rule6))] Gary is furry.[(triple3)] Gary is green.[(triple4 OR ((triple1) -> rule4) OR ((triple2) -> rule5) OR ((triple1 triple2) -> rule2) OR ((((triple3) -> rule7)) -> rule5) OR ((((triple7 triple3) -> rule6)) -> rule5) OR ((((triple7 triple6) -> rule3)) -> rule4) OR ((triple1 ((triple3) -> rule7)) -> rule2) OR ((triple1 ((triple7 triple3) -> rule6)) -> rule2) OR ((((triple7 triple6) -> rule3) triple2) -> rule2) OR ((((triple7 triple6) -> rule3) ((triple3) -> rule7)) -> rule2) OR ((((triple7 triple6) -> rule3) ((triple7 triple3) -> rule6)) -> rule2))] Gary is quiet.[(triple5)] Gary is round.[(triple6 OR ((triple4) -> rule8) OR ((((triple1) -> rule4)) -> rule8) OR ((((triple2) -> rule5)) -> rule8) OR ((((triple1 triple2) -> rule2)) -> rule8) OR ((((((triple3) -> rule7)) -> rule5)) -> rule8) OR ((((((triple7 triple3) -> rule6)) -> rule5)) -> rule8) OR ((((triple1 ((triple3) -> rule7)) -> rule2)) -> rule8) OR ((((triple1 ((triple7 triple3) -> rule6)) -> rule2)) -> rule8))] Gary is young.[(triple7)]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
((triple4 triple7) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple7 triple6) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple7 ((triple4) -> (rule8 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple2) -> (rule5 % int2)) triple7) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((triple7 ((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2)) triple7) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((((triple7 triple3) -> (rule6 % int3))) -> (rule5 % int2)) triple7) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple7 ((((((triple3) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
((triple7 ((((((triple7 triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
triple2
((triple3) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple7 triple3) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
((triple1) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple2) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple1 triple2) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple7 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple7 triple6) -> (rule3 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple1 ((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((triple1 ((triple7 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple7 triple6) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple7 triple6) -> (rule3 % int3)) ((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((triple7 triple6) -> (rule3 % int3)) ((triple7 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
((triple4) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple1 triple2) -> (rule2 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((((triple7 triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple1 ((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple1 ((triple7 triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
triple7