Anne is red. Dave is not furry. Erin is quiet. If something is round then it is not furry. All round things are not kind. All quiet things are kind. If something is kind and not quiet then it is nice. If something is red then it is not blue. All kind things are red. If Dave is red and Dave is not quiet then Dave is blue. Blue, kind things are round.
Anne is red.
("Anne" "is" "red" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
If something is round then it is not furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "-"))
All round things are not kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "-"))
All quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is kind and not quiet then it is nice.
((("something" "is" "kind" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "nice" "+"))
If something is red then it is not blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "-"))
All kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Dave is red and Dave is not quiet then Dave is blue.
((("Dave" "is" "red" "+") ("Dave" "is" "quiet" "~")) -> ("Dave" "is" "blue" "+"))
Blue, kind things are round.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Erin is quiet.
True
1
proof
[(triple3)]
("Erin" "is" "quiet" "+")
triple3
Dave is furry.
False
1
inv-proof
[(triple2)]
("Dave" "is" "furry" "+")
triple2
Anne is not blue.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "blue" "-")
((triple1) -> (rule5 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is blue.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Erin is red.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("Erin" "is" "red" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6))]
("Erin" "is" "red" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not blue.
True
4
proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule5))]
("Erin" "is" "blue" "-")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is blue.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule5))]
("Erin" "is" "blue" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Dave is not red.
Unknown
inv-rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "blue" "+")
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is round.
Unknown
rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is red.[(triple1)] Dave is not furry.[(triple2)] Erin is quiet.[(triple3)] @1: Anne is not blue.[(((triple1) -> rule5))] Erin is kind.[(((triple3) -> rule3))] @2: Erin is red.[(((((triple3) -> rule3)) -> rule6))] @3: Erin is not blue.[(((((((triple3) -> rule3)) -> rule6)) -> rule5))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Dave is not furry.
("Dave" "is" "furry" "-")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Anne is not blue.
("Anne" "is" "blue" "-")
((triple1) -> (rule5 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3