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