Bob is cold. Bob is furry. Bob is kind. Bob is nice. Bob is red. Bob is rough. Bob is smart. Charlie is cold. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is red. Charlie is rough. Charlie is smart. All smart people are furry. If Charlie is cold and Charlie is kind then Charlie is nice. All red people are cold. If Charlie is smart then Charlie is kind. Furry, cold people are kind. Nice, red people are kind.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
All smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If Charlie is cold and Charlie is kind then Charlie is nice.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "nice" "+"))
All red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is smart then Charlie is kind.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "kind" "+"))
Furry, cold people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Nice, red people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Charlie is furry.
True
1
proof
[(triple9 OR ((triple14) -> rule1))]
("Charlie" "is" "furry" "+")
triple9
((triple14) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Bob is not red.
False
1
inv-proof
[(triple5)]
("Bob" "is" "red" "-")
triple5
@0: Bob is cold.[(triple1 OR ((triple5) -> rule3))] Bob is furry.[(triple2 OR ((triple7) -> rule1))] Bob is kind.[(triple3 OR ((triple2 triple1) -> rule5) OR ((triple4 triple5) -> rule6) OR ((triple2 ((triple5) -> rule3)) -> rule5) OR ((((triple7) -> rule1) triple1) -> rule5) OR ((((triple7) -> rule1) ((triple5) -> rule3)) -> rule5))] Bob is nice.[(triple4)] Bob is red.[(triple5)] Bob is rough.[(triple6)] Bob is smart.[(triple7)] Charlie is cold.[(triple8 OR ((triple12) -> rule3))] Charlie is furry.[(triple9 OR ((triple14) -> rule1))] Charlie is kind.[(triple10 OR ((triple14) -> rule4) OR ((triple11 triple12) -> rule6) OR ((triple9 triple8) -> rule5) OR ((triple9 ((triple12) -> rule3)) -> rule5) OR ((((triple14) -> rule1) triple8) -> rule5) OR ((((triple14) -> rule1) ((triple12) -> rule3)) -> rule5))] Charlie is nice.[(triple11 OR ((triple8 triple10) -> rule2) OR ((triple8 ((triple14) -> rule4)) -> rule2) OR ((triple8 ((triple9 triple8) -> rule5)) -> rule2) OR ((((triple12) -> rule3) triple10) -> rule2) OR ((((triple12) -> rule3) ((triple14) -> rule4)) -> rule2) OR ((((triple12) -> rule3) ((triple9 triple8) -> rule5)) -> rule2) OR ((triple8 ((triple9 ((triple12) -> rule3)) -> rule5)) -> rule2) OR ((triple8 ((((triple14) -> rule1) triple8) -> rule5)) -> rule2) OR ((triple8 ((((triple14) -> rule1) ((triple12) -> rule3)) -> rule5)) -> rule2) OR ((((triple12) -> rule3) ((triple9 ((triple12) -> rule3)) -> rule5)) -> rule2) OR ((((triple12) -> rule3) ((((triple14) -> rule1) triple8) -> rule5)) -> rule2) OR ((((triple12) -> rule3) ((((triple14) -> rule1) ((triple12) -> rule3)) -> rule5)) -> rule2))] Charlie is red.[(triple12)] Charlie is rough.[(triple13)] Charlie is smart.[(triple14)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple5) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple7) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple2 triple1) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple4 triple5) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2 ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple7) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
triple8
((triple12) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
((triple14) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
((triple14) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple11 triple12) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple9 triple8) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple9 ((triple12) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple14) -> (rule1 % int2)) triple8) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple14) -> (rule1 % int3)) ((triple12) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple11
((triple8 triple10) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple8 ((triple14) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((triple8 ((triple9 triple8) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple12) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple12) -> (rule3 % int3)) ((triple14) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple12) -> (rule3 % int3)) ((triple9 triple8) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((triple8 ((triple9 ((triple12) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((triple8 ((((triple14) -> (rule1 % int3)) triple8) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((triple8 ((((triple14) -> (rule1 % int4)) ((triple12) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
((((triple12) -> (rule3 % int3)) ((triple9 ((triple12) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple12) -> (rule3 % int4)) ((((triple14) -> (rule1 % int3)) triple8) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
((((triple12) -> (rule3 % int4)) ((((triple14) -> (rule1 % int3)) ((triple12) -> (rule3 % int4))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
triple12
Charlie is rough.
("Charlie" "is" "rough" "+")
triple13
Charlie is smart.
("Charlie" "is" "smart" "+")
triple14