Bob is big. Bob is cold. Bob is kind. Bob is nice. Bob is red. Bob is rough. Bob is smart. If Bob is nice then Bob is smart. Smart people are cold. If Bob is cold and Bob is smart then Bob is kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
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" "+")
If Bob is nice then Bob is smart.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "smart" "+"))
Smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If Bob is cold and Bob is smart then Bob is kind.
((("Bob" "is" "cold" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "kind" "+"))
Bob is cold.
True
1
proof
[(triple2 OR ((triple7) -> rule2) OR ((((triple4) -> rule1)) -> rule2))]
("Bob" "is" "cold" "+")
triple2
((triple7) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not rough.
False
1
inv-proof
[(triple6)]
("Bob" "is" "rough" "-")
triple6
@0: Bob is big.[(triple1)] Bob is cold.[(triple2 OR ((triple7) -> rule2) OR ((((triple4) -> rule1)) -> rule2))] Bob is kind.[(triple3 OR ((triple2 triple7) -> rule3) OR ((triple2 ((triple4) -> rule1)) -> rule3) OR ((((triple7) -> rule2) triple7) -> rule3) OR ((((triple7) -> rule2) ((triple4) -> rule1)) -> rule3) OR ((((((triple4) -> rule1)) -> rule2) triple7) -> rule3) OR ((((((triple4) -> rule1)) -> rule2) ((triple4) -> rule1)) -> rule3))] Bob is nice.[(triple4)] Bob is red.[(triple5)] Bob is rough.[(triple6)] Bob is smart.[(triple7 OR ((triple4) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple7) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple2 triple7) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple7) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple7) -> (rule2 % int3)) ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2)) ((triple4) -> (rule1 % int3))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
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
((triple4) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1