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