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