Anne is round. Anne is smart. Bob is green. Dave is green. Dave is quiet. Erin is furry. Erin is green. Erin is rough. Erin is round. Erin is white. If someone is green and white then they are furry. Round, green people are white. All quiet, smart people are furry. All furry people are white. All green, quiet people are round. If someone is round and furry then they are smart. Quiet, smart people are rough.
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is green.
("Bob" "is" "green" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
If someone is green and white then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Round, green people are white.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
All quiet, smart people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
All green, quiet people are round.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is round and furry then they are smart.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Quiet, smart people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Erin is round.
True
1
proof
[(triple9)]
("Erin" "is" "round" "+")
triple9
Erin is not furry.
False
1
inv-proof
[(triple6 OR ((triple7 triple10) -> rule1) OR ((triple7 ((triple9 triple7) -> rule2)) -> rule1))]
("Erin" "is" "furry" "-")
triple6
((triple7 triple10) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple7 ((triple9 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
True
3
proof
[(((triple9 triple6) -> rule6) OR ((triple9 ((triple7 triple10) -> rule1)) -> rule6) OR ((triple9 ((triple7 ((triple9 triple7) -> rule2)) -> rule1)) -> rule6))]
("Erin" "is" "smart" "+")
((triple9 triple6) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple9 ((triple7 triple10) -> (rule1 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((triple9 ((triple7 ((triple9 triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is not smart.
False
3
inv-proof
[(((triple9 triple6) -> rule6) OR ((triple9 ((triple7 triple10) -> rule1)) -> rule6) OR ((triple9 ((triple7 ((triple9 triple7) -> rule2)) -> rule1)) -> rule6))]
("Erin" "is" "smart" "-")
((triple9 triple6) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple9 ((triple7 triple10) -> (rule1 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((triple9 ((triple7 ((triple9 triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Dave is white.
True
5
proof
[(((((triple4 triple5) -> rule5) triple4) -> rule2))]
("Dave" "is" "white" "+")
((((triple4 triple5) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not white.
False
5
inv-proof
[(((((triple4 triple5) -> rule5) triple4) -> rule2))]
("Dave" "is" "white" "-")
((((triple4 triple5) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
True
7
proof
[(((triple4 ((((triple4 triple5) -> rule5) triple4) -> rule2)) -> rule1))]
("Dave" "is" "furry" "+")
((triple4 ((((triple4 triple5) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not furry.
False
7
inv-proof
[(((triple4 ((((triple4 triple5) -> rule5) triple4) -> rule2)) -> rule1))]
("Dave" "is" "furry" "-")
((triple4 ((((triple4 triple5) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is smart.
True
11
proof
[(((((triple4 triple5) -> rule5) ((triple4 ((((triple4 triple5) -> rule5) triple4) -> rule2)) -> rule1)) -> rule6))]
("Dave" "is" "smart" "+")
((((triple4 triple5) -> (rule5 % int4)) ((triple4 ((((triple4 triple5) -> (rule5 % int4)) triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is not smart.
False
11
inv-proof
[(((((triple4 triple5) -> rule5) ((triple4 ((((triple4 triple5) -> rule5) triple4) -> rule2)) -> rule1)) -> rule6))]
("Dave" "is" "smart" "-")
((((triple4 triple5) -> (rule5 % int4)) ((triple4 ((((triple4 triple5) -> (rule5 % int4)) triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is rough.
True
13
proof
[(((triple5 ((((triple4 triple5) -> rule5) ((triple4 ((((triple4 triple5) -> rule5) triple4) -> rule2)) -> rule1)) -> rule6)) -> rule7))]
("Dave" "is" "rough" "+")
((triple5 ((((triple4 triple5) -> (rule5 % int5)) ((triple4 ((((triple4 triple5) -> (rule5 % int5)) triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
Dave is not rough.
False
13
inv-proof
[(((triple5 ((((triple4 triple5) -> rule5) ((triple4 ((((triple4 triple5) -> rule5) triple4) -> rule2)) -> rule1)) -> rule6)) -> rule7))]
("Dave" "is" "rough" "-")
((triple5 ((((triple4 triple5) -> (rule5 % int5)) ((triple4 ((((triple4 triple5) -> (rule5 % int5)) triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not furry.
Unknown
inv-rconc
[@3: Bob is furry.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule5 <- FAIL)]]
("Bob" "is" "furry" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "rough" "+")
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is white.
Unknown
rconc
[@2: Anne is white.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Anne is round.[(triple1)] Anne is smart.[(triple2)] Bob is green.[(triple3)] Dave is green.[(triple4)] Dave is quiet.[(triple5)] Erin is furry.[(triple6 OR ((triple7 triple10) -> rule1) OR ((triple7 ((triple9 triple7) -> rule2)) -> rule1))] Erin is green.[(triple7)] Erin is rough.[(triple8)] Erin is round.[(triple9)] Erin is white.[(triple10 OR ((triple6) -> rule4) OR ((triple9 triple7) -> rule2))] @1: Dave is round.[(((triple4 triple5) -> rule5))] Erin is smart.[(((triple9 triple6) -> rule6) OR ((triple9 ((triple7 triple10) -> rule1)) -> rule6) OR ((triple9 ((triple7 ((triple9 triple7) -> rule2)) -> rule1)) -> rule6))] @2: Dave is white.[(((((triple4 triple5) -> rule5) triple4) -> rule2))] @3: Dave is furry.[(((triple4 ((((triple4 triple5) -> rule5) triple4) -> rule2)) -> rule1))] @4: Dave is smart.[(((((triple4 triple5) -> rule5) ((triple4 ((((triple4 triple5) -> rule5) triple4) -> rule2)) -> rule1)) -> rule6))] @5: Dave is rough.[(((triple5 ((((triple4 triple5) -> rule5) ((triple4 ((((triple4 triple5) -> rule5) triple4) -> rule2)) -> rule1)) -> rule6)) -> rule7))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple6
((triple7 triple10) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple7 ((triple9 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple8
Erin is round.
("Erin" "is" "round" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
((triple6) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple9 triple7) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple4 triple5) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple9 triple6) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple9 ((triple7 triple10) -> (rule1 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((triple9 ((triple7 ((triple9 triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((triple4 triple5) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((triple4 ((((triple4 triple5) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((triple4 triple5) -> (rule5 % int4)) ((triple4 ((((triple4 triple5) -> (rule5 % int4)) triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
((triple5 ((((triple4 triple5) -> (rule5 % int5)) ((triple4 ((((triple4 triple5) -> (rule5 % int5)) triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5