Anne is not red. Bob is cold. Erin is kind. Fiona is red. Rough things are quiet. Red things are quiet. All smart things are rough. If something is quiet and not cold then it is not rough. If Fiona is cold then Fiona is rough. If something is quiet then it is smart.
Anne is not red.
("Anne" "is" "red" "-")
Bob is cold.
("Bob" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
All smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is quiet and not cold then it is not rough.
((("something" "is" "quiet" "+") ("something" "is" "cold" "~")) -> ("something" "is" "rough" "-"))
If Fiona is cold then Fiona is rough.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "rough" "+"))
If something is quiet then it is smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Anne is not red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Fiona is not red.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "red" "-")
triple4
Fiona is quiet.
True
2
proof
[(((triple4) -> rule2))]
("Fiona" "is" "quiet" "+")
((triple4) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is not quiet.
False
2
inv-proof
[(((triple4) -> rule2))]
("Fiona" "is" "quiet" "-")
((triple4) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
True
3
proof
[(((((triple4) -> rule2)) -> rule6))]
("Fiona" "is" "smart" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule6))]
("Fiona" "is" "smart" "-")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is rough.
True
4
proof
[(((((((triple4) -> rule2)) -> rule6)) -> rule3))]
("Fiona" "is" "rough" "+")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is not rough.
False
4
inv-proof
[(((((((triple4) -> rule2)) -> rule6)) -> rule3))]
("Fiona" "is" "rough" "-")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Anne is not rough.
Unknown
inv-rconc
[@3: Anne is rough.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Erin is rough.
Unknown
rconc
[@3: Erin is rough.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule1 <- FAIL)]]
("Erin" "is" "rough" "+")
Anne is not quiet.
Unknown
inv-rconc
[@4: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule6 <- rule2 <- FAIL)]]
("Anne" "is" "quiet" "-")
Bob is rough.
Unknown
rconc
[@3: Bob is rough.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule1 <- FAIL)]]
("Bob" "is" "rough" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is not red.[(triple1)] Bob is cold.[(triple2)] Erin is kind.[(triple3)] Fiona is red.[(triple4)] @1: Fiona is quiet.[(((triple4) -> rule2))] @2: Fiona is smart.[(((((triple4) -> rule2)) -> rule6))] @3: Fiona is rough.[(((((((triple4) -> rule2)) -> rule6)) -> rule3))]
Anne is not red.
("Anne" "is" "red" "-")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
triple4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple4) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3