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