Anne is furry. Anne is white. Bob is furry. Kind things are red. All kind, white things are furry. If Anne is furry then Anne is rough. All nice things are kind. All nice things are kind. If Anne is white then Anne is red. All rough, kind things are white. All rough, white things are nice.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
All kind, white things are furry.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If Anne is furry then Anne is rough.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "rough" "+"))
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If Anne is white then Anne is red.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "red" "+"))
All rough, kind things are white.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
All rough, white things are nice.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Anne is white.
True
1
proof
[(triple2)]
("Anne" "is" "white" "+")
triple2
Bob is not furry.
False
1
inv-proof
[(triple3)]
("Bob" "is" "furry" "-")
triple3
Anne is rough.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple2) -> rule6) OR ((((((((triple1) -> rule3) triple2) -> rule8)) -> rule4)) -> rule1) OR ((((((((triple1) -> rule3) triple2) -> rule8)) -> rule5)) -> rule1))]
("Anne" "is" "red" "-")
((triple2) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((((((triple1) -> (rule3 % int4)) triple2) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
((((((((triple1) -> (rule3 % int4)) triple2) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is nice.
True
4
proof
[(((((triple1) -> rule3) triple2) -> rule8))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not nice.
False
4
inv-proof
[(((((triple1) -> rule3) triple2) -> rule8))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule3 % int2)) triple2) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is kind.
True
5
proof
[(((((((triple1) -> rule3) triple2) -> rule8)) -> rule4) OR ((((((triple1) -> rule3) triple2) -> rule8)) -> rule5))]
("Anne" "is" "kind" "+")
((((((triple1) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((((triple1) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not kind.
False
5
inv-proof
[(((((((triple1) -> rule3) triple2) -> rule8)) -> rule4) OR ((((((triple1) -> rule3) triple2) -> rule8)) -> rule5))]
("Anne" "is" "kind" "-")
((((((triple1) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((((triple1) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is red.
Unknown
rconc
[@3: Bob is red.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule8 <- FAIL)]]
("Bob" "is" "red" "+")
Bob is not kind.
Unknown
inv-rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "white" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Anne is furry.[(triple1)] Anne is white.[(triple2)] Bob is furry.[(triple3)] @1: Anne is red.[(((triple2) -> rule6) OR ((((((((triple1) -> rule3) triple2) -> rule8)) -> rule4)) -> rule1) OR ((((((((triple1) -> rule3) triple2) -> rule8)) -> rule5)) -> rule1))] Anne is rough.[(((triple1) -> rule3))] @2: Anne is nice.[(((((triple1) -> rule3) triple2) -> rule8))] @3: Anne is kind.[(((((((triple1) -> rule3) triple2) -> rule8)) -> rule4) OR ((((((triple1) -> rule3) triple2) -> rule8)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
((triple2) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((((((triple1) -> (rule3 % int4)) triple2) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
((((((((triple1) -> (rule3 % int4)) triple2) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple1) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((((triple1) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3