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