Anne is smart. Dave is round. Erin is furry. All blue things are not furry. All round things are blue. If something is round then it is blue. Furry, smart things are quiet. If something is quiet and not blue then it is red. If Anne is round and Anne is not furry then Anne is young. If something is blue and not furry then it is smart. All red things are young.
Anne is smart.
("Anne" "is" "smart" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is furry.
("Erin" "is" "furry" "+")
All blue things are not furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "-"))
All round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Furry, smart things are quiet.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and not blue then it is red.
((("something" "is" "quiet" "+") ("something" "is" "blue" "~")) -> ("something" "is" "red" "+"))
If Anne is round and Anne is not furry then Anne is young.
((("Anne" "is" "round" "+") ("Anne" "is" "furry" "~")) -> ("Anne" "is" "young" "+"))
If something is blue and not furry then it is smart.
((("something" "is" "blue" "+") ("something" "is" "furry" "~")) -> ("something" "is" "smart" "+"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Dave is round.
True
1
proof
[(triple2)]
("Dave" "is" "round" "+")
triple2
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Dave is blue.
True
2
proof
[(((triple2) -> rule2) OR ((triple2) -> rule3))]
("Dave" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple2) -> rule2) OR ((triple2) -> rule3))]
("Dave" "is" "blue" "-")
((triple2) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not furry.
True
3
proof
[(((((triple2) -> rule2)) -> rule1) OR ((((triple2) -> rule3)) -> rule1))]
("Dave" "is" "furry" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is furry.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1) OR ((((triple2) -> rule3)) -> rule1))]
("Dave" "is" "furry" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
True
6
proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule7) OR ((((triple2) -> rule2) ((((triple2) -> rule3)) -> rule1)) -> rule7) OR ((((triple2) -> rule3) ((((triple2) -> rule2)) -> rule1)) -> rule7) OR ((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule1)) -> rule7))]
("Dave" "is" "smart" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not smart.
False
6
inv-proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule7) OR ((((triple2) -> rule2) ((((triple2) -> rule3)) -> rule1)) -> rule7) OR ((((triple2) -> rule3) ((((triple2) -> rule2)) -> rule1)) -> rule7) OR ((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule1)) -> rule7))]
("Dave" "is" "smart" "-")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "red" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "red" "+")
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "quiet" "-")
Erin is young.
Unknown
rconc
[@2: Erin is young.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Erin" "is" "young" "+")
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" "+")
@0: Anne is smart.[(triple1)] Dave is round.[(triple2)] Erin is furry.[(triple3)] @1: Dave is blue.[(((triple2) -> rule2) OR ((triple2) -> rule3))] @2: Dave is not furry.[(((((triple2) -> rule2)) -> rule1) OR ((((triple2) -> rule3)) -> rule1))] @3: Dave is smart.[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule7) OR ((((triple2) -> rule2) ((((triple2) -> rule3)) -> rule1)) -> rule7) OR ((((triple2) -> rule3) ((((triple2) -> rule2)) -> rule1)) -> rule7) OR ((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule1)) -> rule7))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3