Anne is quiet. Bob is furry. Bob is rough. Bob is white. Dave is round. Dave is white. Erin is white. All round, quiet things are nice. Furry things are rough. All round things are furry. If Erin is quiet and Erin is round then Erin is not furry. All rough things are quiet. If Dave is quiet and Dave is big then Dave is not white. If something is white and nice then it is not big.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is white.
("Erin" "is" "white" "+")
All round, quiet things are nice.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
Furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If Erin is quiet and Erin is round then Erin is not furry.
((("Erin" "is" "quiet" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "furry" "-"))
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If Dave is quiet and Dave is big then Dave is not white.
((("Dave" "is" "quiet" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "white" "-"))
If something is white and nice then it is not big.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "-"))
Bob is white.
True
1
proof
[(triple4)]
("Bob" "is" "white" "+")
triple4
Bob is not furry.
False
1
inv-proof
[(triple2)]
("Bob" "is" "furry" "-")
triple2
Bob is quiet.
True
2
proof
[(((triple3) -> rule5) OR ((((triple2) -> rule2)) -> rule5))]
("Bob" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not quiet.
False
2
inv-proof
[(((triple3) -> rule5) OR ((((triple2) -> rule2)) -> rule5))]
("Bob" "is" "quiet" "-")
((triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Dave is rough.
True
3
proof
[(((((triple5) -> rule3)) -> rule2))]
("Dave" "is" "rough" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule2))]
("Dave" "is" "rough" "-")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
True
4
proof
[(((((((triple5) -> rule3)) -> rule2)) -> rule5))]
("Dave" "is" "quiet" "+")
((((((triple5) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not quiet.
False
4
inv-proof
[(((((((triple5) -> rule3)) -> rule2)) -> rule5))]
("Dave" "is" "quiet" "-")
((((((triple5) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
True
6
proof
[(((triple5 ((((((triple5) -> rule3)) -> rule2)) -> rule5)) -> rule1))]
("Dave" "is" "nice" "+")
((triple5 ((((((triple5) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is not nice.
False
6
inv-proof
[(((triple5 ((((((triple5) -> rule3)) -> rule2)) -> rule5)) -> rule1))]
("Dave" "is" "nice" "-")
((triple5 ((((((triple5) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is not big.
True
8
proof
[(((triple6 ((triple5 ((((((triple5) -> rule3)) -> rule2)) -> rule5)) -> rule1)) -> rule7))]
("Dave" "is" "big" "-")
((triple6 ((triple5 ((((((triple5) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5
Dave is big.
False
8
inv-proof
[(((triple6 ((triple5 ((((((triple5) -> rule3)) -> rule2)) -> rule5)) -> rule1)) -> rule7))]
("Dave" "is" "big" "+")
((triple6 ((triple5 ((((((triple5) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "-")
Erin is quiet.
Unknown
rconc
[@3: Erin is quiet.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule3 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not rough.
Unknown
inv-rconc
[@2: Erin is rough.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Erin" "is" "rough" "-")
Anne is rough.
Unknown
rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "furry" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "nice" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is quiet.[(triple1)] Bob is furry.[(triple2)] Bob is rough.[(triple3 OR ((triple2) -> rule2))] Bob is white.[(triple4)] Dave is round.[(triple5)] Dave is white.[(triple6)] Erin is white.[(triple7)] @1: Bob is quiet.[(((triple3) -> rule5) OR ((((triple2) -> rule2)) -> rule5))] Dave is furry.[(((triple5) -> rule3))] @2: Dave is rough.[(((((triple5) -> rule3)) -> rule2))] @3: Dave is quiet.[(((((((triple5) -> rule3)) -> rule2)) -> rule5))] @4: Dave is nice.[(((triple5 ((((((triple5) -> rule3)) -> rule2)) -> rule5)) -> rule1))] @5: Dave is not big.[(((triple6 ((triple5 ((((((triple5) -> rule3)) -> rule2)) -> rule5)) -> rule1)) -> rule7))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
((triple2) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple5) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((triple5 ((((((triple5) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is not big.
("Dave" "is" "big" "-")
((triple6 ((triple5 ((((((triple5) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5