Anne is nice. Anne is quiet. Dave is young. Erin is cold. Fiona is blue. Fiona is not nice. Fiona is white. Young, blue people are not nice. If Dave is white then Dave is young. Cold people are blue. All cold people are blue. All blue people are young. Quiet, nice people are young. All white people are quiet. If Fiona is nice then Fiona is blue.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is not nice.
("Fiona" "is" "nice" "-")
Fiona is white.
("Fiona" "is" "white" "+")
Young, blue people are not nice.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "-"))
If Dave is white then Dave is young.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "young" "+"))
Cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
All cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
All blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Quiet, nice people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If Fiona is nice then Fiona is blue.
((("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "blue" "+"))
Erin is cold.
True
1
proof
[(triple4)]
("Erin" "is" "cold" "+")
triple4
Fiona is not blue.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "blue" "-")
triple5
Fiona is quiet.
True
2
proof
[(((triple7) -> rule7))]
("Fiona" "is" "quiet" "+")
((triple7) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple4) -> rule3) OR ((triple4) -> rule4))]
("Erin" "is" "blue" "-")
((triple4) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple4) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
True
3
proof
[(((((triple4) -> rule3)) -> rule5) OR ((((triple4) -> rule4)) -> rule5))]
("Erin" "is" "young" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not young.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule5) OR ((((triple4) -> rule4)) -> rule5))]
("Erin" "is" "young" "-")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not nice.
True
6
proof
[(((((((triple4) -> rule3)) -> rule5) ((triple4) -> rule3)) -> rule1) OR ((((((triple4) -> rule3)) -> rule5) ((triple4) -> rule4)) -> rule1) OR ((((((triple4) -> rule4)) -> rule5) ((triple4) -> rule3)) -> rule1) OR ((((((triple4) -> rule4)) -> rule5) ((triple4) -> rule4)) -> rule1))]
("Erin" "is" "nice" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2)) ((triple4) -> (rule3 % int3))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2)) ((triple4) -> (rule4 % int3))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2)) ((triple4) -> (rule3 % int3))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2)) ((triple4) -> (rule4 % int3))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is nice.
False
6
inv-proof
[(((((((triple4) -> rule3)) -> rule5) ((triple4) -> rule3)) -> rule1) OR ((((((triple4) -> rule3)) -> rule5) ((triple4) -> rule4)) -> rule1) OR ((((((triple4) -> rule4)) -> rule5) ((triple4) -> rule3)) -> rule1) OR ((((((triple4) -> rule4)) -> rule5) ((triple4) -> rule4)) -> rule1))]
("Erin" "is" "nice" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2)) ((triple4) -> (rule3 % int3))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2)) ((triple4) -> (rule4 % int3))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2)) ((triple4) -> (rule3 % int3))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2)) ((triple4) -> (rule4 % int3))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "quiet" "+")
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "blue" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "quiet" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Anne is nice.[(triple1)] Anne is quiet.[(triple2)] Dave is young.[(triple3)] Erin is cold.[(triple4)] Fiona is blue.[(triple5)] Fiona is not nice.[(triple6 OR ((((triple5) -> rule5) triple5) -> rule1))] Fiona is white.[(triple7)] @1: Anne is young.[(((triple2 triple1) -> rule6))] Erin is blue.[(((triple4) -> rule3) OR ((triple4) -> rule4))] Fiona is quiet.[(((triple7) -> rule7))] Fiona is young.[(((triple5) -> rule5))] @2: Erin is young.[(((((triple4) -> rule3)) -> rule5) OR ((((triple4) -> rule4)) -> rule5))] @3: Erin is not nice.[(((((((triple4) -> rule3)) -> rule5) ((triple4) -> rule3)) -> rule1) OR ((((((triple4) -> rule3)) -> rule5) ((triple4) -> rule4)) -> rule1) OR ((((((triple4) -> rule4)) -> rule5) ((triple4) -> rule3)) -> rule1) OR ((((((triple4) -> rule4)) -> rule5) ((triple4) -> rule4)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is not nice.
("Fiona" "is" "nice" "-")
triple6
((((triple5) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Anne is young.
("Anne" "is" "young" "+")
((triple2 triple1) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple4) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple4) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple7) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple5) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not nice.
("Erin" "is" "nice" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2)) ((triple4) -> (rule3 % int3))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2)) ((triple4) -> (rule4 % int3))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2)) ((triple4) -> (rule3 % int3))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2)) ((triple4) -> (rule4 % int3))) -> (rule1 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3