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