Anne is round. Bob is round. Fiona is rough. Gary is furry. Gary is rough. Gary is round. Gary is white. If someone is nice then they are round. If Anne is nice and Anne is white then Anne is round. All nice, round people are furry. Nice, red people are round. Quiet people are nice. Rough, quiet people are red. All round people are quiet. All furry, round people are quiet. If someone is furry then they are rough.
Anne is round.
("Anne" "is" "round" "+")
Bob is round.
("Bob" "is" "round" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If Anne is nice and Anne is white then Anne is round.
((("Anne" "is" "nice" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "round" "+"))
All nice, round people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
Nice, red people are round.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Rough, quiet people are red.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
All round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
All furry, round people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Gary is white.
True
1
proof
[(triple7)]
("Gary" "is" "white" "+")
triple7
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Anne is quiet.
True
2
proof
[(((triple1) -> rule7))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule7))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Gary is nice.
True
3
proof
[(((((triple6) -> rule7)) -> rule5) OR ((((triple4 triple6) -> rule8)) -> rule5))]
("Gary" "is" "nice" "+")
((((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple4 triple6) -> (rule8 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Anne is not nice.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule5))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Bob is furry.
True
5
proof
[(((((((triple2) -> rule7)) -> rule5) triple2) -> rule3))]
("Bob" "is" "furry" "+")
((((((triple2) -> (rule7 % int3))) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not furry.
False
5
inv-proof
[(((((((triple2) -> rule7)) -> rule5) triple2) -> rule3))]
("Bob" "is" "furry" "-")
((((((triple2) -> (rule7 % int3))) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is rough.
True
6
proof
[(((((((((triple2) -> rule7)) -> rule5) triple2) -> rule3)) -> rule9))]
("Bob" "is" "rough" "+")
((((((((triple2) -> (rule7 % int4))) -> (rule5 % int3)) triple2) -> (rule3 % int2))) -> (rule9 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is not rough.
False
6
inv-proof
[(((((((((triple2) -> rule7)) -> rule5) triple2) -> rule3)) -> rule9))]
("Bob" "is" "rough" "-")
((((((((triple2) -> (rule7 % int4))) -> (rule5 % int3)) triple2) -> (rule3 % int2))) -> (rule9 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is red.
True
9
proof
[(((((((((((triple2) -> rule7)) -> rule5) triple2) -> rule3)) -> rule9) ((triple2) -> rule7)) -> rule6))]
("Bob" "is" "red" "+")
((((((((((triple2) -> (rule7 % int5))) -> (rule5 % int4)) triple2) -> (rule3 % int3))) -> (rule9 % int2)) ((triple2) -> (rule7 % int5))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
int5
Bob is not red.
False
9
inv-proof
[(((((((((((triple2) -> rule7)) -> rule5) triple2) -> rule3)) -> rule9) ((triple2) -> rule7)) -> rule6))]
("Bob" "is" "red" "-")
((((((((((triple2) -> (rule7 % int5))) -> (rule5 % int4)) triple2) -> (rule3 % int3))) -> (rule9 % int2)) ((triple2) -> (rule7 % int5))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
int5
Fiona is not red.
Unknown
inv-rconc
[@6: Fiona is red.[CWA. Example of deepest failure = (rule6 <- rule7 <- rule1 <- rule5 <- rule8 <- rule3 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is nice.
Unknown
rconc
[@3: Fiona is nice.[CWA. Example of deepest failure = (rule5 <- rule7 <- rule1 <- FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not furry.
Unknown
inv-rconc
[@4: Fiona is furry.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule7 <- rule1 <- FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is quiet.
Unknown
rconc
[@5: Fiona is quiet.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule5 <- rule8 <- rule3 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not round.
Unknown
inv-rconc
[@4: Fiona is round.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule7 <- rule4 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is round.[(triple1)] Bob is round.[(triple2)] Fiona is rough.[(triple3)] Gary is furry.[(triple4 OR ((((((triple6) -> rule7)) -> rule5) triple6) -> rule3))] Gary is rough.[(triple5 OR ((triple4) -> rule9) OR ((((((((triple6) -> rule7)) -> rule5) triple6) -> rule3)) -> rule9))] Gary is round.[(triple6)] Gary is white.[(triple7)] @1: Anne is quiet.[(((triple1) -> rule7))] Bob is quiet.[(((triple2) -> rule7))] Gary is quiet.[(((triple6) -> rule7) OR ((triple4 triple6) -> rule8))] @2: Anne is nice.[(((((triple1) -> rule7)) -> rule5))] Bob is nice.[(((((triple2) -> rule7)) -> rule5))] Gary is nice.[(((((triple6) -> rule7)) -> rule5) OR ((((triple4 triple6) -> rule8)) -> rule5))] Gary is red.[(((triple5 ((triple6) -> rule7)) -> rule6) OR ((triple5 ((triple4 triple6) -> rule8)) -> rule6) OR ((((triple4) -> rule9) ((triple6) -> rule7)) -> rule6) OR ((((triple4) -> rule9) ((triple4 triple6) -> rule8)) -> rule6) OR ((((((((((triple6) -> rule7)) -> rule5) triple6) -> rule3)) -> rule9) ((triple6) -> rule7)) -> rule6) OR ((((((((((triple6) -> rule7)) -> rule5) triple6) -> rule3)) -> rule9) ((triple4 triple6) -> rule8)) -> rule6))] @3: Anne is furry.[(((((((triple1) -> rule7)) -> rule5) triple1) -> rule3))] Bob is furry.[(((((((triple2) -> rule7)) -> rule5) triple2) -> rule3))] @4: Anne is rough.[(((((((((triple1) -> rule7)) -> rule5) triple1) -> rule3)) -> rule9))] Bob is rough.[(((((((((triple2) -> rule7)) -> rule5) triple2) -> rule3)) -> rule9))] @5: Anne is red.[(((((((((((triple1) -> rule7)) -> rule5) triple1) -> rule3)) -> rule9) ((triple1) -> rule7)) -> rule6))] Bob is red.[(((((((((((triple2) -> rule7)) -> rule5) triple2) -> rule3)) -> rule9) ((triple2) -> rule7)) -> rule6))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
((((((triple6) -> (rule7 % int3))) -> (rule5 % int2)) triple6) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
triple5
((triple4) -> (rule9 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((((((triple6) -> (rule7 % int4))) -> (rule5 % int3)) triple6) -> (rule3 % int2))) -> (rule9 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple6) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple4 triple6) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple4 triple6) -> (rule8 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple5 ((triple6) -> (rule7 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((triple5 ((triple4 triple6) -> (rule8 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple4) -> (rule9 % int3)) ((triple6) -> (rule7 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((triple4) -> (rule9 % int3)) ((triple4 triple6) -> (rule8 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((((((triple6) -> (rule7 % int5))) -> (rule5 % int4)) triple6) -> (rule3 % int3))) -> (rule9 % int2)) ((triple6) -> (rule7 % int5))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
((((((((((triple6) -> (rule7 % int5))) -> (rule5 % int4)) triple6) -> (rule3 % int3))) -> (rule9 % int2)) ((triple4 triple6) -> (rule8 % int5))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
Anne is furry.
("Anne" "is" "furry" "+")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple2) -> (rule7 % int3))) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule5 % int3)) triple1) -> (rule3 % int2))) -> (rule9 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
((((((((triple2) -> (rule7 % int4))) -> (rule5 % int3)) triple2) -> (rule3 % int2))) -> (rule9 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
((((((((((triple1) -> (rule7 % int5))) -> (rule5 % int4)) triple1) -> (rule3 % int3))) -> (rule9 % int2)) ((triple1) -> (rule7 % int5))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
Bob is red.
("Bob" "is" "red" "+")
((((((((((triple2) -> (rule7 % int5))) -> (rule5 % int4)) triple2) -> (rule3 % int3))) -> (rule9 % int2)) ((triple2) -> (rule7 % int5))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
int5