Dave is furry. Dave is nice. Dave is rough. Erin is furry. Gary is red. Harry is kind. Harry is not rough. Rough things are smart. All red things are kind. If something is smart then it is nice. Red, kind things are rough. If something is green and not furry then it is not rough. If something is red and not furry then it is not rough. Furry things are red. If Harry is kind and Harry is nice then Harry is green.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Red, kind things are rough.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is green and not furry then it is not rough.
((("something" "is" "green" "+") ("something" "is" "furry" "~")) -> ("something" "is" "rough" "-"))
If something is red and not furry then it is not rough.
((("something" "is" "red" "+") ("something" "is" "furry" "~")) -> ("something" "is" "rough" "-"))
Furry things are red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If Harry is kind and Harry is nice then Harry is green.
((("Harry" "is" "kind" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "green" "+"))
Erin is furry.
True
1
proof
[(triple4)]
("Erin" "is" "furry" "+")
triple4
Dave is not furry.
False
1
inv-proof
[(triple1)]
("Dave" "is" "furry" "-")
triple1
Gary is kind.
True
2
proof
[(((triple5) -> rule2))]
("Gary" "is" "kind" "+")
((triple5) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple3) -> rule1) OR ((((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule2)) -> rule4)) -> rule1))]
("Dave" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((((triple1) -> (rule7 % int4)) ((((triple1) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is kind.
True
3
proof
[(((((triple1) -> rule7)) -> rule2))]
("Dave" "is" "kind" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule2))]
("Dave" "is" "kind" "-")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Erin is rough.
True
6
proof
[(((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule2)) -> rule4))]
("Erin" "is" "rough" "+")
((((triple4) -> (rule7 % int3)) ((((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not rough.
False
6
inv-proof
[(((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule2)) -> rule4))]
("Erin" "is" "rough" "-")
((((triple4) -> (rule7 % int3)) ((((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Gary is nice.
True
6
proof
[(((((((triple5 ((triple5) -> rule2)) -> rule4)) -> rule1)) -> rule3))]
("Gary" "is" "nice" "+")
((((((triple5 ((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Erin is not smart.
False
7
inv-proof
[(((((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule2)) -> rule4)) -> rule1))]
("Erin" "is" "smart" "-")
((((((triple4) -> (rule7 % int4)) ((((triple4) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is nice.
True
8
proof
[(((((((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule2)) -> rule4)) -> rule1)) -> rule3))]
("Erin" "is" "nice" "+")
((((((((triple4) -> (rule7 % int5)) ((((triple4) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5
Erin is not nice.
False
8
inv-proof
[(((((((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule2)) -> rule4)) -> rule1)) -> rule3))]
("Erin" "is" "nice" "-")
((((((((triple4) -> (rule7 % int5)) ((((triple4) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is nice.
Unknown
rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Harry" "is" "nice" "+")
Harry is not green.
Unknown
inv-rconc
[@3: Harry is green.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule1 <- FAIL)]]
("Harry" "is" "green" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "smart" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Dave is furry.[(triple1)] Dave is nice.[(triple2 OR ((((triple3) -> rule1)) -> rule3) OR ((((((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule2)) -> rule4)) -> rule1)) -> rule3))] Dave is rough.[(triple3 OR ((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule2)) -> rule4))] Erin is furry.[(triple4)] Gary is red.[(triple5)] Harry is kind.[(triple6)] Harry is not rough.[(triple7)] @1: Dave is red.[(((triple1) -> rule7))] Dave is smart.[(((triple3) -> rule1) OR ((((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule2)) -> rule4)) -> rule1))] Erin is red.[(((triple4) -> rule7))] Gary is kind.[(((triple5) -> rule2))] @2: Dave is kind.[(((((triple1) -> rule7)) -> rule2))] Erin is kind.[(((((triple4) -> rule7)) -> rule2))] Gary is rough.[(((triple5 ((triple5) -> rule2)) -> rule4))] @3: Erin is rough.[(((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule2)) -> rule4))] Gary is smart.[(((((triple5 ((triple5) -> rule2)) -> rule4)) -> rule1))] @4: Erin is smart.[(((((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule2)) -> rule4)) -> rule1))] Gary is nice.[(((((((triple5 ((triple5) -> rule2)) -> rule4)) -> rule1)) -> rule3))] @5: Erin is nice.[(((((((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule2)) -> rule4)) -> rule1)) -> rule3))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((((((triple1) -> (rule7 % int5)) ((((triple1) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
Dave is rough.
("Dave" "is" "rough" "+")
triple3
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is not rough.
("Harry" "is" "rough" "-")
triple7
Dave is red.
("Dave" "is" "red" "+")
((triple1) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((((triple1) -> (rule7 % int4)) ((((triple1) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
((triple4) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple5) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple5 ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple4) -> (rule7 % int3)) ((((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((((triple5 ((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple4) -> (rule7 % int4)) ((((triple4) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
((((((triple5 ((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
((((((((triple4) -> (rule7 % int5)) ((((triple4) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5