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