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