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