Charlie is white. Dave is white. Erin is smart. Harry is round. Kind people are not smart. All blue people are smart. Furry people are kind. If Dave is blue and Dave is white then Dave is round. All white people are furry. All kind, blue people are round. If Dave is kind and Dave is rough then Dave is not white. All blue, smart people are white.
Charlie is white.
("Charlie" "is" "white" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is round.
("Harry" "is" "round" "+")
Kind people are not smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "-"))
All blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If Dave is blue and Dave is white then Dave is round.
((("Dave" "is" "blue" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "round" "+"))
All white people are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
All kind, blue people are round.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Dave is kind and Dave is rough then Dave is not white.
((("Dave" "is" "kind" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "white" "-"))
All blue, smart people are white.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Dave is white.
True
1
proof
[(triple2)]
("Dave" "is" "white" "+")
triple2
Charlie is not white.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "white" "-")
triple1
Dave is furry.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is kind.
True
3
proof
[(((((triple2) -> rule5)) -> rule3))]
("Dave" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Charlie is not kind.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("Charlie" "is" "kind" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not smart.
True
4
proof
[(((((((triple1) -> rule5)) -> rule3)) -> rule1))]
("Charlie" "is" "smart" "-")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Dave is smart.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule3)) -> rule1))]
("Dave" "is" "smart" "+")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Harry is not furry.
Unknown
inv-rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is kind.
Unknown
rconc
[@3: Harry is kind.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule8 <- FAIL)]]
("Harry" "is" "kind" "+")
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "round" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "smart" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is white.[(triple1)] Dave is white.[(triple2)] Erin is smart.[(triple3)] Harry is round.[(triple4)] @1: Charlie is furry.[(((triple1) -> rule5))] Dave is furry.[(((triple2) -> rule5))] @2: Charlie is kind.[(((((triple1) -> rule5)) -> rule3))] Dave is kind.[(((((triple2) -> rule5)) -> rule3))] @3: Charlie is not smart.[(((((((triple1) -> rule5)) -> rule3)) -> rule1))] Dave is not smart.[(((((((triple2) -> rule5)) -> rule3)) -> rule1))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Charlie is not smart.
("Charlie" "is" "smart" "-")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Dave is not smart.
("Dave" "is" "smart" "-")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3