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