Bob is furry. Bob is red. Dave is round. Fiona is furry. Fiona is kind. Fiona is nice. Fiona is white. Gary is furry. Gary is kind. Gary is nice. If someone is rough then they are red. Nice, red people are furry. Furry people are nice. All round people are rough. If someone is furry then they are round. If someone is round then they are white. If someone is nice then they are kind. If someone is kind then they are white.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
If someone is rough then they are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Nice, red people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry then they are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Bob is red.
True
1
proof
[(triple2 OR ((((((triple1) -> rule5)) -> rule4)) -> rule1))]
("Bob" "is" "red" "+")
triple2
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Gary is not kind.
False
1
inv-proof
[(triple9 OR ((triple10) -> rule7) OR ((((triple8) -> rule3)) -> rule7))]
("Gary" "is" "kind" "-")
triple9
((triple10) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Bob is nice.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "round" "-")
((triple1) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule7))]
("Bob" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule6) OR ((((((triple1) -> rule3)) -> rule7)) -> rule8))]
("Bob" "is" "white" "-")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Gary is red.
True
4
proof
[(((((((triple8) -> rule5)) -> rule4)) -> rule1))]
("Gary" "is" "red" "+")
((((((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is not red.
False
4
inv-proof
[(((((((triple8) -> rule5)) -> rule4)) -> rule1))]
("Gary" "is" "red" "-")
((((((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is kind.
Unknown
rconc
[@3: Dave is kind.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule2 <- FAIL)]]
("Dave" "is" "kind" "+")
@0: Bob is furry.[(triple1)] Bob is red.[(triple2 OR ((((((triple1) -> rule5)) -> rule4)) -> rule1))] Dave is round.[(triple3)] Fiona is furry.[(triple4)] Fiona is kind.[(triple5 OR ((triple6) -> rule7) OR ((((triple4) -> rule3)) -> rule7))] Fiona is nice.[(triple6 OR ((triple4) -> rule3))] Fiona is white.[(triple7 OR ((triple5) -> rule8) OR ((((triple4) -> rule5)) -> rule6) OR ((((triple6) -> rule7)) -> rule8) OR ((((((triple4) -> rule3)) -> rule7)) -> rule8))] Gary is furry.[(triple8)] Gary is kind.[(triple9 OR ((triple10) -> rule7) OR ((((triple8) -> rule3)) -> rule7))] Gary is nice.[(triple10 OR ((triple8) -> rule3))] @1: Bob is nice.[(((triple1) -> rule3))] Bob is round.[(((triple1) -> rule5))] Dave is rough.[(((triple3) -> rule4))] Dave is white.[(((triple3) -> rule6))] Fiona is round.[(((triple4) -> rule5))] Gary is round.[(((triple8) -> rule5))] Gary is white.[(((triple9) -> rule8) OR ((((triple10) -> rule7)) -> rule8) OR ((((triple8) -> rule5)) -> rule6) OR ((((((triple8) -> rule3)) -> rule7)) -> rule8))] @2: Bob is kind.[(((((triple1) -> rule3)) -> rule7))] Bob is rough.[(((((triple1) -> rule5)) -> rule4))] Bob is white.[(((((triple1) -> rule5)) -> rule6) OR ((((((triple1) -> rule3)) -> rule7)) -> rule8))] Dave is red.[(((((triple3) -> rule4)) -> rule1))] Fiona is rough.[(((((triple4) -> rule5)) -> rule4))] Gary is rough.[(((((triple8) -> rule5)) -> rule4))] @3: Fiona is red.[(((((((triple4) -> rule5)) -> rule4)) -> rule1))] Gary is red.[(((((((triple8) -> rule5)) -> rule4)) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
triple3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
((triple6) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
((triple4) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple7
((triple5) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
((triple10) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple10
((triple8) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple4) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple8) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple9) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple10) -> (rule7 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple8) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((triple8) -> (rule5 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3