Bob is big. Bob is cold. Bob is kind. Bob is nice. Bob is quiet. Bob is red. Bob is rough. Red things are nice. All rough, nice things are cold. If something is big then it is rough. Red things are quiet. All rough, red things are quiet. If something is nice then it 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 quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
All rough, nice things are cold.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is big then it is rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
All rough, red things are quiet.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If something is nice then it is kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Bob is red.
True
1
proof
[(triple6)]
("Bob" "is" "red" "+")
triple6
Bob is not cold.
False
1
inv-proof
[(triple2 OR ((triple7 triple4) -> rule2) OR ((triple7 ((triple6) -> rule1)) -> rule2) OR ((((triple1) -> rule3) triple4) -> rule2) OR ((((triple1) -> rule3) ((triple6) -> rule1)) -> rule2))]
("Bob" "is" "cold" "-")
triple2
((triple7 triple4) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple7 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple1) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple1) -> (rule3 % int3)) ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
@0: Bob is big.[(triple1)] Bob is cold.[(triple2 OR ((triple7 triple4) -> rule2) OR ((triple7 ((triple6) -> rule1)) -> rule2) OR ((((triple1) -> rule3) triple4) -> rule2) OR ((((triple1) -> rule3) ((triple6) -> rule1)) -> rule2))] Bob is kind.[(triple3 OR ((triple4) -> rule6) OR ((((triple6) -> rule1)) -> rule6))] Bob is nice.[(triple4 OR ((triple6) -> rule1))] Bob is quiet.[(triple5 OR ((triple6) -> rule4) OR ((triple7 triple6) -> rule5) OR ((((triple1) -> rule3) triple6) -> rule5))] Bob is red.[(triple6)] Bob is rough.[(triple7 OR ((triple1) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple7 triple4) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple7 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple1) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple1) -> (rule3 % int3)) ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple4) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple6) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple6) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple7 triple6) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple1) -> (rule3 % int2)) triple6) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple6
Bob is rough.
("Bob" "is" "rough" "+")
triple7
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1