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