Bob is furry. Bob is white. Charlie is big. Charlie is cold. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is round. Dave is cold. Dave is nice. Dave is round. Dave is white. Fiona is big. Fiona is cold. Fiona is furry. Fiona is white. If someone is nice then they are round. If someone is nice and round then they are kind. If Charlie is nice then Charlie is cold.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is nice and round then they are kind.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is nice then Charlie is cold.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "cold" "+"))
Fiona is furry.
True
1
proof
[(triple15)]
("Fiona" "is" "furry" "+")
triple15
Charlie is not round.
False
1
inv-proof
[(triple8 OR ((triple7) -> rule1))]
("Charlie" "is" "round" "-")
triple8
((triple7) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is kind.
True
3
proof
[(((triple10 triple11) -> rule2) OR ((triple10 ((triple10) -> rule1)) -> rule2))]
("Dave" "is" "kind" "+")
((triple10 triple11) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple10 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((triple10 triple11) -> rule2) OR ((triple10 ((triple10) -> rule1)) -> rule2))]
("Dave" "is" "kind" "-")
((triple10 triple11) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple10 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "kind" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "kind" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Bob is furry.[(triple1)] Bob is white.[(triple2)] Charlie is big.[(triple3)] Charlie is cold.[(triple4 OR ((triple7) -> rule3))] Charlie is furry.[(triple5)] Charlie is kind.[(triple6 OR ((triple7 triple8) -> rule2) OR ((triple7 ((triple7) -> rule1)) -> rule2))] Charlie is nice.[(triple7)] Charlie is round.[(triple8 OR ((triple7) -> rule1))] Dave is cold.[(triple9)] Dave is nice.[(triple10)] Dave is round.[(triple11 OR ((triple10) -> rule1))] Dave is white.[(triple12)] Fiona is big.[(triple13)] Fiona is cold.[(triple14)] Fiona is furry.[(triple15)] Fiona is white.[(triple16)] @1: Dave is kind.[(((triple10 triple11) -> rule2) OR ((triple10 ((triple10) -> rule1)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
((triple7) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
((triple7 triple8) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple7 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
triple8
((triple7) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is nice.
("Dave" "is" "nice" "+")
triple10
Dave is round.
("Dave" "is" "round" "+")
triple11
((triple10) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple12
Fiona is big.
("Fiona" "is" "big" "+")
triple13
Fiona is cold.
("Fiona" "is" "cold" "+")
triple14
Fiona is furry.
("Fiona" "is" "furry" "+")
triple15
Fiona is white.
("Fiona" "is" "white" "+")
triple16
Dave is kind.
("Dave" "is" "kind" "+")
((triple10 triple11) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple10 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2