Anne is young. Bob is cold. Bob is not quiet. Bob is red. Bob is not young. Dave is red. Erin is quiet. If someone is blue then they are young. Quiet people are young. Young people are quiet. If someone is blue and round then they are not quiet. If Erin is red then Erin is blue. Blue people are kind. Young people are cold. Quiet, cold people are blue. Kind, young people are red.
Anne is young.
("Anne" "is" "young" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is not young.
("Bob" "is" "young" "-")
Dave is red.
("Dave" "is" "red" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If someone is blue then they are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
Young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If someone is blue and round then they are not quiet.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "-"))
If Erin is red then Erin is blue.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "blue" "+"))
Blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Quiet, cold people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Kind, young people are red.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Bob is cold.
True
1
proof
[(triple2)]
("Bob" "is" "cold" "+")
triple2
Anne is not young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "-")
triple1
Anne is quiet.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Erin is cold.
True
3
proof
[(((((triple7) -> rule2)) -> rule7))]
("Erin" "is" "cold" "+")
((((triple7) -> (rule2 % int2))) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Anne is not blue.
False
5
inv-proof
[(((((triple1) -> rule3) ((triple1) -> rule7)) -> rule8))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Erin is blue.
True
5
proof
[(((triple7 ((((triple7) -> rule2)) -> rule7)) -> rule8))]
("Erin" "is" "blue" "+")
((triple7 ((((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Anne is not kind.
False
6
inv-proof
[(((((((triple1) -> rule3) ((triple1) -> rule7)) -> rule8)) -> rule6))]
("Anne" "is" "kind" "-")
((((((triple1) -> (rule3 % int4)) ((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Erin is kind.
True
6
proof
[(((((triple7 ((((triple7) -> rule2)) -> rule7)) -> rule8)) -> rule6))]
("Erin" "is" "kind" "+")
((((triple7 ((((triple7) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is not kind.
False
6
inv-proof
[(((((triple7 ((((triple7) -> rule2)) -> rule7)) -> rule8)) -> rule6))]
("Erin" "is" "kind" "-")
((((triple7 ((((triple7) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is red.
True
9
proof
[(((((((triple7 ((((triple7) -> rule2)) -> rule7)) -> rule8)) -> rule6) ((triple7) -> rule2)) -> rule9))]
("Erin" "is" "red" "+")
((((((triple7 ((((triple7) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) ((triple7) -> (rule2 % int5))) -> (rule9 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5
Erin is not red.
False
9
inv-proof
[(((((((triple7 ((((triple7) -> rule2)) -> rule7)) -> rule8)) -> rule6) ((triple7) -> rule2)) -> rule9))]
("Erin" "is" "red" "-")
((((((triple7 ((((triple7) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) ((triple7) -> (rule2 % int5))) -> (rule9 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5
Dave is not young.
Unknown
inv-rconc
[@4: Dave is young.[CWA. Example of deepest failure = (rule1 <- rule8 <- rule3 <- rule2 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is blue.
Unknown
rconc
[@3: Dave is blue.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule1 <- FAIL)]]
("Dave" "is" "blue" "+")
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "blue" "-")
Dave is quiet.
Unknown
rconc
[@3: Dave is quiet.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule8 <- FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not cold.
Unknown
inv-rconc
[@5: Dave is cold.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule3 <- rule1 <- rule8 <- FAIL)]]
("Dave" "is" "cold" "-")
Bob is kind.
Unknown
rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("Bob" "is" "kind" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Anne is young.[(triple1)] Bob is cold.[(triple2)] Bob is not quiet.[(triple3)] Bob is not young.[(triple5)] Bob is red.[(triple4)] Dave is red.[(triple6)] Erin is quiet.[(triple7)] @1: Anne is cold.[(((triple1) -> rule7))] Anne is quiet.[(((triple1) -> rule3))] Erin is young.[(((triple7) -> rule2))] @2: Anne is blue.[(((((triple1) -> rule3) ((triple1) -> rule7)) -> rule8))] Erin is cold.[(((((triple7) -> rule2)) -> rule7))] @3: Anne is kind.[(((((((triple1) -> rule3) ((triple1) -> rule7)) -> rule8)) -> rule6))] Erin is blue.[(((triple7 ((((triple7) -> rule2)) -> rule7)) -> rule8))] @4: Anne is red.[(((((((((triple1) -> rule3) ((triple1) -> rule7)) -> rule8)) -> rule6) triple1) -> rule9))] Erin is kind.[(((((triple7 ((((triple7) -> rule2)) -> rule7)) -> rule8)) -> rule6))] @5: Erin is red.[(((((((triple7 ((((triple7) -> rule2)) -> rule7)) -> rule8)) -> rule6) ((triple7) -> rule2)) -> rule9))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple3
Bob is not young.
("Bob" "is" "young" "-")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple7) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((((triple7) -> (rule2 % int2))) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple1) -> (rule3 % int4)) ((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
((triple7 ((((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((((((((triple1) -> (rule3 % int5)) ((triple1) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) triple1) -> (rule9 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
Erin is kind.
("Erin" "is" "kind" "+")
((((triple7 ((((triple7) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
((((((triple7 ((((triple7) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) ((triple7) -> (rule2 % int5))) -> (rule9 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5