Charlie is rough. Dave is rough. Harry is not furry. If someone is furry then they are rough. Rough people are furry. Furry people are not red. If Dave is furry and Dave is white then Dave is not green. If someone is furry and not red then they are white. If someone is white and not green then they are kind.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Furry people are not red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "-"))
If Dave is furry and Dave is white then Dave is not green.
((("Dave" "is" "furry" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "green" "-"))
If someone is furry and not red then they are white.
((("someone" "is" "furry" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "white" "+"))
If someone is white and not green then they are kind.
((("someone" "is" "white" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "kind" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Dave is furry.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is not red.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Dave" "is" "red" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is red.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Dave" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Charlie is white.
True
6
proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule5))]
("Charlie" "is" "white" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Dave is not white.
False
6
inv-proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule5))]
("Dave" "is" "white" "-")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "kind" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "kind" "+")
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Charlie is rough.[(triple1)] Dave is rough.[(triple2)] Harry is not furry.[(triple3)] @1: Charlie is furry.[(((triple1) -> rule2))] Dave is furry.[(((triple2) -> rule2))] @2: Charlie is not red.[(((((triple1) -> rule2)) -> rule3))] Dave is not red.[(((((triple2) -> rule2)) -> rule3))] @3: Charlie is white.[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule5))] Dave is white.[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule5))] @4: Dave is not green.[(((((triple2) -> rule2) ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule5)) -> rule4))] @5: Dave is kind.[(((((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule5) ((((triple2) -> rule2) ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule5)) -> rule4)) -> rule6))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Harry is not furry.
("Harry" "is" "furry" "-")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Dave is not red.
("Dave" "is" "red" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not green.
("Dave" "is" "green" "-")
((((triple2) -> (rule2 % int4)) ((((triple2) -> (rule2 % int4)) ((((triple2) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not red.
("Dave" "is" "red" "-")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple2) -> (rule2 % int5)) ((((triple2) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule2 % int5)) ((((triple2) -> (rule2 % int5)) ((((triple2) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not green.
("Dave" "is" "green" "-")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not red.
("Dave" "is" "red" "-")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5