Charlie is rough. Dave is furry. Dave is rough. All rough, furry people are young. If someone is young then they are nice. If someone is white then they are young. If someone is rough and nice then they are red. If Charlie is furry then Charlie is nice. Young people are red. Nice people are white. Red people are furry.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is rough.
("Dave" "is" "rough" "+")
All rough, furry people are young.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone is white then they are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If someone is rough and nice then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If Charlie is furry then Charlie is nice.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "nice" "+"))
Young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Dave is rough.
True
1
proof
[(triple3)]
("Dave" "is" "rough" "+")
triple3
Dave is not rough.
False
1
inv-proof
[(triple3)]
("Dave" "is" "rough" "-")
triple3
Dave is young.
True
3
proof
[(((triple3 triple2) -> rule1))]
("Dave" "is" "young" "+")
((triple3 triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
3
inv-proof
[(((triple3 triple2) -> rule1))]
("Dave" "is" "young" "-")
((triple3 triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
True
4
proof
[(((((triple3 triple2) -> rule1)) -> rule6) OR ((triple3 ((((triple3 triple2) -> rule1)) -> rule2)) -> rule4))]
("Dave" "is" "red" "+")
((((triple3 triple2) -> (rule1 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((triple3 ((((triple3 triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not nice.
False
4
inv-proof
[(((((triple3 triple2) -> rule1)) -> rule2))]
("Dave" "is" "nice" "-")
((((triple3 triple2) -> (rule1 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Charlie is not nice.
Unknown
inv-rconc
[@7: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule8 <- rule6 <- rule3 <- rule7 <- rule5 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is furry.
Unknown
rconc
[@6: Charlie is furry.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule2 <- rule3 <- rule7 <- rule5 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not white.
Unknown
inv-rconc
[@6: Charlie is white.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule1 <- rule8 <- rule4 <- rule5 <- FAIL)]]
("Charlie" "is" "white" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Charlie is rough.[(triple1)] Dave is furry.[(triple2)] Dave is rough.[(triple3)] @1: Dave is young.[(((triple3 triple2) -> rule1))] @2: Dave is nice.[(((((triple3 triple2) -> rule1)) -> rule2))] Dave is red.[(((((triple3 triple2) -> rule1)) -> rule6) OR ((triple3 ((((triple3 triple2) -> rule1)) -> rule2)) -> rule4))] @3: Dave is white.[(((((((triple3 triple2) -> rule1)) -> rule2)) -> rule7))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
((triple3 triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple3 triple2) -> (rule1 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple3 triple2) -> (rule1 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((triple3 ((((triple3 triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((((triple3 triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3