Bob is big. Bob is furry. Bob is nice. Bob is red. Bob is round. Bob is smart. Bob is young. Gary is big. Gary is furry. Gary is nice. Gary is red. Gary is round. Gary is smart. Gary is young. Big people are young. If Gary is nice then Gary is big. Smart, red people are round. If someone is young and smart then they are furry. Round, red people are furry. All nice people are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If Gary is nice then Gary is big.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "big" "+"))
Smart, red people are round.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is young and smart then they are furry.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Round, red people are furry.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Gary is furry.
True
1
proof
[(triple9 OR ((triple12 triple11) -> rule5) OR ((triple14 triple13) -> rule4) OR ((((triple8) -> rule1) triple13) -> rule4) OR ((((triple13 triple11) -> rule3) triple11) -> rule5) OR ((((((triple10) -> rule2)) -> rule1) triple13) -> rule4) OR ((((((triple10) -> rule6)) -> rule1) triple13) -> rule4))]
("Gary" "is" "furry" "+")
triple9
((triple12 triple11) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple14 triple13) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple8) -> (rule1 % int2)) triple13) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple13 triple11) -> (rule3 % int2)) triple11) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple10) -> (rule2 % int3))) -> (rule1 % int2)) triple13) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple10) -> (rule6 % int3))) -> (rule1 % int2)) triple13) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not nice.
False
1
inv-proof
[(triple10)]
("Gary" "is" "nice" "-")
triple10
@0: Bob is big.[(triple1 OR ((triple3) -> rule6))] Bob is furry.[(triple2 OR ((triple5 triple4) -> rule5) OR ((triple7 triple6) -> rule4) OR ((((triple1) -> rule1) triple6) -> rule4) OR ((((triple6 triple4) -> rule3) triple4) -> rule5) OR ((((((triple3) -> rule6)) -> rule1) triple6) -> rule4))] Bob is nice.[(triple3)] Bob is red.[(triple4)] Bob is round.[(triple5 OR ((triple6 triple4) -> rule3))] Bob is smart.[(triple6)] Bob is young.[(triple7 OR ((triple1) -> rule1) OR ((((triple3) -> rule6)) -> rule1))] Gary is big.[(triple8 OR ((triple10) -> rule2) OR ((triple10) -> rule6))] Gary is furry.[(triple9 OR ((triple12 triple11) -> rule5) OR ((triple14 triple13) -> rule4) OR ((((triple8) -> rule1) triple13) -> rule4) OR ((((triple13 triple11) -> rule3) triple11) -> rule5) OR ((((((triple10) -> rule2)) -> rule1) triple13) -> rule4) OR ((((((triple10) -> rule6)) -> rule1) triple13) -> rule4))] Gary is nice.[(triple10)] Gary is red.[(triple11)] Gary is round.[(triple12 OR ((triple13 triple11) -> rule3))] Gary is smart.[(triple13)] Gary is young.[(triple14 OR ((triple8) -> rule1) OR ((((triple10) -> rule2)) -> rule1) OR ((((triple10) -> rule6)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple5 triple4) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple7 triple6) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple1) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple6 triple4) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple6 triple4) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple8
((triple10) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple10) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple9
((triple12 triple11) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple14 triple13) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple8) -> (rule1 % int2)) triple13) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple13 triple11) -> (rule3 % int2)) triple11) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple10) -> (rule2 % int3))) -> (rule1 % int2)) triple13) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple10) -> (rule6 % int3))) -> (rule1 % int2)) triple13) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
((triple13 triple11) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple13
Gary is young.
("Gary" "is" "young" "+")
triple14
((triple8) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple10) -> (rule6 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2