Anne is smart. Bob is kind. Bob is white. Furry things are not rough. All smart things are rough. If something is furry and cold then it is kind. If something is cold then it is quiet. If Bob is smart and Bob is not furry then Bob is not cold. Cold things are smart. If something is kind then it is cold. If something is smart and not kind then it is white.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Furry things are not rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "-"))
All smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is furry and cold then it is kind.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is cold then it is quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If Bob is smart and Bob is not furry then Bob is not cold.
((("Bob" "is" "smart" "+") ("Bob" "is" "furry" "~")) -> ("Bob" "is" "cold" "-"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is kind then it is cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something is smart and not kind then it is white.
((("something" "is" "smart" "+") ("something" "is" "kind" "~")) -> ("something" "is" "white" "+"))
Bob is white.
True
1
proof
[(triple3)]
("Bob" "is" "white" "+")
triple3
Bob is not white.
False
1
inv-proof
[(triple3)]
("Bob" "is" "white" "-")
triple3
Bob is cold.
True
2
proof
[(((triple2) -> rule7))]
("Bob" "is" "cold" "+")
((triple2) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple2) -> rule7))]
("Bob" "is" "cold" "-")
((triple2) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
True
3
proof
[(((((triple2) -> rule7)) -> rule6))]
("Bob" "is" "smart" "+")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule4))]
("Bob" "is" "quiet" "-")
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
True
4
proof
[(((((((triple2) -> rule7)) -> rule6)) -> rule2))]
("Bob" "is" "rough" "+")
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not rough.
False
4
inv-proof
[(((((((triple2) -> rule7)) -> rule6)) -> rule2))]
("Bob" "is" "rough" "-")
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is quiet.
Unknown
rconc
[@3: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule3 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is smart.[(triple1)] Bob is kind.[(triple2)] Bob is white.[(triple3)] @1: Anne is rough.[(((triple1) -> rule2))] Bob is cold.[(((triple2) -> rule7))] @2: Bob is quiet.[(((((triple2) -> rule7)) -> rule4))] Bob is smart.[(((((triple2) -> rule7)) -> rule6))] @3: Bob is rough.[(((((((triple2) -> rule7)) -> rule6)) -> rule2))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3