Anne is red. Bob is cold. Dave is kind. Cold things are nice. If Bob is blue then Bob is cold. All cold, white things are blue. All white, cold things are nice. If something is nice then it is white. If Anne is nice and Anne is blue then Anne is red.
Anne is red.
("Anne" "is" "red" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If Bob is blue then Bob is cold.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "cold" "+"))
All cold, white things are blue.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
All white, cold things are nice.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Anne is nice and Anne is blue then Anne is red.
((("Anne" "is" "nice" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "red" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Bob is not cold.
False
1
inv-proof
[(triple2)]
("Bob" "is" "cold" "-")
triple2
Bob is nice.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "nice" "-")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
True
3
proof
[(((((triple2) -> rule1)) -> rule5))]
("Bob" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("Bob" "is" "white" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
True
5
proof
[(((triple2 ((((triple2) -> rule1)) -> rule5)) -> rule3))]
("Bob" "is" "blue" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not blue.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule1)) -> rule5)) -> rule3))]
("Bob" "is" "blue" "-")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "nice" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is white.
Unknown
rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Dave" "is" "white" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is red.[(triple1)] Bob is cold.[(triple2)] Dave is kind.[(triple3)] @1: Bob is nice.[(((triple2) -> rule1))] @2: Bob is white.[(((((triple2) -> rule1)) -> rule5))] @3: Bob is blue.[(((triple2 ((((triple2) -> rule1)) -> rule5)) -> rule3))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3