Bob is big. Bob is cold. Bob is furry. Bob is green. Bob is kind. Bob is nice. Bob is rough. If someone is cold and big then they are rough. All cold people are kind. Green, cold people are nice. If Bob is cold and Bob is rough then Bob is nice. All green people are big. Cold, big people are furry. Rough people are kind. Cold people are green.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
If someone is cold and big then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Green, cold people are nice.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If Bob is cold and Bob is rough then Bob is nice.
((("Bob" "is" "cold" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "nice" "+"))
All green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Cold, big people are furry.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Bob is rough.
True
1
proof
[(triple7 OR ((triple2 triple1) -> rule1) OR ((triple2 ((triple4) -> rule5)) -> rule1) OR ((triple2 ((((triple2) -> rule8)) -> rule5)) -> rule1))]
("Bob" "is" "rough" "+")
triple7
((triple2 triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple2 ((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((triple2 ((((triple2) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not nice.
False
1
inv-proof
[(triple6 OR ((triple2 triple7) -> rule4) OR ((triple4 triple2) -> rule3) OR ((triple2 ((triple2 triple1) -> rule1)) -> rule4) OR ((((triple2) -> rule8) triple2) -> rule3) OR ((triple2 ((triple2 ((triple4) -> rule5)) -> rule1)) -> rule4) OR ((triple2 ((triple2 ((((triple2) -> rule8)) -> rule5)) -> rule1)) -> rule4))]
("Bob" "is" "nice" "-")
triple6
((triple2 triple7) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple4 triple2) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2 ((triple2 triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple2) -> (rule8 % int2)) triple2) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple2 ((triple2 ((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((triple2 ((triple2 ((((triple2) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
@0: Bob is big.[(triple1 OR ((triple4) -> rule5) OR ((((triple2) -> rule8)) -> rule5))] Bob is cold.[(triple2)] Bob is furry.[(triple3 OR ((triple2 triple1) -> rule6) OR ((triple2 ((triple4) -> rule5)) -> rule6) OR ((triple2 ((((triple2) -> rule8)) -> rule5)) -> rule6))] Bob is green.[(triple4 OR ((triple2) -> rule8))] Bob is kind.[(triple5 OR ((triple2) -> rule2) OR ((triple7) -> rule7) OR ((((triple2 triple1) -> rule1)) -> rule7) OR ((((triple2 ((triple4) -> rule5)) -> rule1)) -> rule7) OR ((((triple2 ((((triple2) -> rule8)) -> rule5)) -> rule1)) -> rule7))] Bob is nice.[(triple6 OR ((triple2 triple7) -> rule4) OR ((triple4 triple2) -> rule3) OR ((triple2 ((triple2 triple1) -> rule1)) -> rule4) OR ((((triple2) -> rule8) triple2) -> rule3) OR ((triple2 ((triple2 ((triple4) -> rule5)) -> rule1)) -> rule4) OR ((triple2 ((triple2 ((((triple2) -> rule8)) -> rule5)) -> rule1)) -> rule4))] Bob is rough.[(triple7 OR ((triple2 triple1) -> rule1) OR ((triple2 ((triple4) -> rule5)) -> rule1) OR ((triple2 ((((triple2) -> rule8)) -> rule5)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple4) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple2 triple1) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple2 ((triple4) -> (rule5 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((triple2 ((((triple2) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
triple4
((triple2) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple5
((triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple7) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple2 triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple2 ((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((triple2 ((((triple2) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
triple6
((triple2 triple7) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple4 triple2) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2 ((triple2 triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple2) -> (rule8 % int2)) triple2) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple2 ((triple2 ((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((triple2 ((triple2 ((((triple2) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
triple7
((triple2 triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple2 ((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((triple2 ((((triple2) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3