Anne is cold. Bob is cold. Bob is kind. Bob is nice. Bob is quiet. Bob is rough. Bob is smart. If something is rough then it is quiet. All kind things are quiet. All kind things are big. Big things are smart. All rough things are smart. All nice things are rough.
Anne is cold.
("Anne" "is" "cold" "+")
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 rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
If something is rough then it is quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
All rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Bob is kind.
True
1
proof
[(triple3)]
("Bob" "is" "kind" "+")
triple3
Bob is not quiet.
False
1
inv-proof
[(triple5 OR ((triple3) -> rule2) OR ((triple6) -> rule1) OR ((((triple4) -> rule6)) -> rule1))]
("Bob" "is" "quiet" "-")
triple5
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is cold.[(triple1)] Bob is cold.[(triple2)] Bob is kind.[(triple3)] Bob is nice.[(triple4)] Bob is quiet.[(triple5 OR ((triple3) -> rule2) OR ((triple6) -> rule1) OR ((((triple4) -> rule6)) -> rule1))] Bob is rough.[(triple6 OR ((triple4) -> rule6))] Bob is smart.[(triple7 OR ((triple6) -> rule5) OR ((((triple3) -> rule3)) -> rule4) OR ((((triple4) -> rule6)) -> rule5))] @1: Bob is big.[(((triple3) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple6
((triple4) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple7
((triple6) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((triple3) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1