Anne is not blue. Anne is not rough. Anne is not smart. Dave is rough. Dave is white. Erin is kind. Erin is smart. Erin is white. Fiona is blue. Fiona is kind. Fiona is white. If someone is quiet and blue then they are smart. All blue, rough people are quiet. All cold people are not quiet. All blue, kind people are not cold. If Dave is smart and Dave is blue then Dave is white. Cold people are white. If someone is white then they are blue. If someone is smart then they are blue. Smart, quiet people are kind.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is not rough.
("Anne" "is" "rough" "-")
Anne is not smart.
("Anne" "is" "smart" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If someone is quiet and blue then they are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
All blue, rough people are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All cold people are not quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "-"))
All blue, kind people are not cold.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "-"))
If Dave is smart and Dave is blue then Dave is white.
((("Dave" "is" "smart" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "white" "+"))
Cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Smart, quiet people are kind.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Fiona is blue.
True
1
proof
[(triple9 OR ((triple11) -> rule7))]
("Fiona" "is" "blue" "+")
triple9
((triple11) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Anne is smart.
False
1
inv-proof
[(triple3)]
("Anne" "is" "smart" "+")
triple3
Dave is blue.
True
2
proof
[(((triple5) -> rule7))]
("Dave" "is" "blue" "+")
((triple5) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple5) -> rule7))]
("Dave" "is" "blue" "-")
((triple5) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
True
4
proof
[(((((triple5) -> rule7) triple4) -> rule2))]
("Dave" "is" "quiet" "+")
((((triple5) -> (rule7 % int2)) triple4) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not quiet.
False
4
inv-proof
[(((((triple5) -> rule7) triple4) -> rule2))]
("Dave" "is" "quiet" "-")
((((triple5) -> (rule7 % int2)) triple4) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
True
7
proof
[(((((((triple5) -> rule7) triple4) -> rule2) ((triple5) -> rule7)) -> rule1))]
("Dave" "is" "smart" "+")
((((((triple5) -> (rule7 % int3)) triple4) -> (rule2 % int2)) ((triple5) -> (rule7 % int3))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not smart.
False
7
inv-proof
[(((((((triple5) -> rule7) triple4) -> rule2) ((triple5) -> rule7)) -> rule1))]
("Dave" "is" "smart" "-")
((((((triple5) -> (rule7 % int3)) triple4) -> (rule2 % int2)) ((triple5) -> (rule7 % int3))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is kind.
True
12
proof
[(((((((((triple5) -> rule7) triple4) -> rule2) ((triple5) -> rule7)) -> rule1) ((((triple5) -> rule7) triple4) -> rule2)) -> rule9))]
("Dave" "is" "kind" "+")
((((((((triple5) -> (rule7 % int4)) triple4) -> (rule2 % int3)) ((triple5) -> (rule7 % int4))) -> (rule1 % int2)) ((((triple5) -> (rule7 % int4)) triple4) -> (rule2 % int3))) -> (rule9 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is not kind.
False
12
inv-proof
[(((((((((triple5) -> rule7) triple4) -> rule2) ((triple5) -> rule7)) -> rule1) ((((triple5) -> rule7) triple4) -> rule2)) -> rule9))]
("Dave" "is" "kind" "-")
((((((((triple5) -> (rule7 % int4)) triple4) -> (rule2 % int3)) ((triple5) -> (rule7 % int4))) -> (rule1 % int2)) ((((triple5) -> (rule7 % int4)) triple4) -> (rule2 % int3))) -> (rule9 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is not cold.
True
15
proof
[(((((triple5) -> rule7) ((((((((triple5) -> rule7) triple4) -> rule2) ((triple5) -> rule7)) -> rule1) ((((triple5) -> rule7) triple4) -> rule2)) -> rule9)) -> rule4))]
("Dave" "is" "cold" "-")
((((triple5) -> (rule7 % int5)) ((((((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4)) ((triple5) -> (rule7 % int5))) -> (rule1 % int3)) ((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4))) -> (rule9 % int2))) -> (rule4 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
Dave is cold.
False
15
inv-proof
[(((((triple5) -> rule7) ((((((((triple5) -> rule7) triple4) -> rule2) ((triple5) -> rule7)) -> rule1) ((((triple5) -> rule7) triple4) -> rule2)) -> rule9)) -> rule4))]
("Dave" "is" "cold" "+")
((((triple5) -> (rule7 % int5)) ((((((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4)) ((triple5) -> (rule7 % int5))) -> (rule1 % int3)) ((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4))) -> (rule9 % int2))) -> (rule4 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Anne" "is" "kind" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "quiet" "+")
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "quiet" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Anne is not blue.[(triple1)] Anne is not rough.[(triple2)] Anne is not smart.[(triple3)] Dave is rough.[(triple4)] Dave is white.[(triple5)] Erin is kind.[(triple6)] Erin is smart.[(triple7)] Erin is white.[(triple8)] Fiona is blue.[(triple9 OR ((triple11) -> rule7))] Fiona is kind.[(triple10)] Fiona is white.[(triple11)] @1: Dave is blue.[(((triple5) -> rule7))] Erin is blue.[(((triple7) -> rule8) OR ((triple8) -> rule7))] Fiona is not cold.[(((triple9 triple10) -> rule4) OR ((((triple11) -> rule7) triple10) -> rule4))] @2: Dave is quiet.[(((((triple5) -> rule7) triple4) -> rule2))] Erin is not cold.[(((((triple7) -> rule8) triple6) -> rule4) OR ((((triple8) -> rule7) triple6) -> rule4))] @3: Dave is smart.[(((((((triple5) -> rule7) triple4) -> rule2) ((triple5) -> rule7)) -> rule1))] @4: Dave is kind.[(((((((((triple5) -> rule7) triple4) -> rule2) ((triple5) -> rule7)) -> rule1) ((((triple5) -> rule7) triple4) -> rule2)) -> rule9))] @5: Dave is not cold.[(((((triple5) -> rule7) ((((((((triple5) -> rule7) triple4) -> rule2) ((triple5) -> rule7)) -> rule1) ((((triple5) -> rule7) triple4) -> rule2)) -> rule9)) -> rule4))]
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is not rough.
("Anne" "is" "rough" "-")
triple2
Anne is not smart.
("Anne" "is" "smart" "-")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
((triple11) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
Fiona is white.
("Fiona" "is" "white" "+")
triple11
Dave is blue.
("Dave" "is" "blue" "+")
((triple5) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple7) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple8) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Fiona is not cold.
("Fiona" "is" "cold" "-")
((triple9 triple10) -> (rule4 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
((((triple11) -> (rule7 % int2)) triple10) -> (rule4 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple5) -> (rule7 % int2)) triple4) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is not cold.
("Erin" "is" "cold" "-")
((((triple7) -> (rule8 % int2)) triple6) -> (rule4 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple8) -> (rule7 % int2)) triple6) -> (rule4 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple5) -> (rule7 % int3)) triple4) -> (rule2 % int2)) ((triple5) -> (rule7 % int3))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((((((triple5) -> (rule7 % int4)) triple4) -> (rule2 % int3)) ((triple5) -> (rule7 % int4))) -> (rule1 % int2)) ((((triple5) -> (rule7 % int4)) triple4) -> (rule2 % int3))) -> (rule9 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is not cold.
("Dave" "is" "cold" "-")
((((triple5) -> (rule7 % int5)) ((((((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4)) ((triple5) -> (rule7 % int5))) -> (rule1 % int3)) ((((triple5) -> (rule7 % int5)) triple4) -> (rule2 % int4))) -> (rule9 % int2))) -> (rule4 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5